1
0
mirror of https://github.com/php/php-src.git synced 2026-04-19 22:11:12 +02:00

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

This commit is contained in:
Derick Rethans
2017-03-20 17:48:15 +00:00
parent 7dd52cbcdd
commit 2b7c3831cd

View File

@@ -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)