Don't truncate subsecond precision in run-tests.php JUNIT output

When run-tests.php has been typed[1], the type of `$time` has been
chosen to be `int`.  This, however, leads to truncation, and the
somewhat relevant subsecond precision is lost.  We fix that by
changing the type to `float`, although `int|string` would be more
appropriate, but requires PHP ≥ 7.4.0.  Another option would be to
move the `number_format()` formatting into `junit_mark_test_as()`.

[1] <11274f5>

Closes GH-7836.

Author: cmb69

run-tests.php

@@ -3478,7 +3478,7 @@ function junit_mark_test_as(
     $type,
     string $file_name,
     string $test_name,
-    ?int $time = null,
+    ?float $time = null,
     string $message = '',
     string $details = ''
 ): void {
@@ -3533,15 +3533,15 @@ function junit_mark_test_as(
     $JUNIT['files'][$file_name]['xml'] .= "</testcase>\n";
 }
 
-function junit_suite_record(string $suite, string $param, int $value = 1): void
+function junit_suite_record(string $suite, string $param, float $value = 1): void
 {
     global $JUNIT;
 
     $JUNIT[$param] += $value;
     $JUNIT['suites'][$suite][$param] += $value;
 }
 
-function junit_get_timer(string $file_name): int
+function junit_get_timer(string $file_name): float
 {
     global $JUNIT;
     if (!junit_enabled()) {