com php-src: Fix for #73837: "new DateTime()" with a cast to double: ext/date/php_date.c

Commit:    2b7c3831cdc9a0e708040af37d8cf8967755bce3
Author:    Derick Rethans <[email protected]>         Mon, 20 Mar 2017 17:48:15 +0000
Parents:   7dd52cbcddbd2af7ea64edc4a3cb337aa68cefe9
Branches:  PHP-7.1

Link:       http://git.php.net/?p=php-src.git;a=commitdiff;h=2b7c3831cdc9a0e708040af37d8cf8967755bce3

Log:
Fix for #73837: "new DateTime()" with a cast to double

Bugs:
https://bugs.php.net/73837

Changed paths:
  M  ext/date/php_date.c


Diff:
diff --git a/ext/date/php_date.c b/ext/date/php_date.c
index 30b40cd..25373d0 100644
--- a/ext/date/php_date.c
+++ b/ext/date/php_date.c
@@ -2548,7 +2548,7 @@ static void update_errors_warnings(timelib_error_container *last_errors) /* {{{
 
 static void php_date_set_time_fraction(timelib_time *time, int microseconds)
 {
-	time->f = microseconds / 1000000;
+	time->f = (double) microseconds / 1000000;
 }
 
 static void php_date_get_current_time_with_fraction(time_t *sec, suseconds_t *usec)