Function filetime_to_seconds

src/engine/execnt.cpp:743–747

 */

static double filetime_to_seconds( FILETIME const ft )
{
    return ft.dwHighDateTime * ( (double)( 1UL << 31 ) * 2.0 * 1.0e-7 ) +
        ft.dwLowDateTime * 1.0e-7;
}


static void record_times( HANDLE const process, timing_info * const time )