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

diff --git a/ext/date/php_date.c b/ext/date/php_date.c
index 30b40cdb9c413067e32df30912ee3b73b82b1905..25373d0f086bbed5ee438a7010d82cc8ece55c0f 100644 (file)
--- 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)