Double & float are the same in PHP

See:
- https://www.php.net/manual/en/migration85.deprecated.php
- https://php.watch/versions/8.5/boolean-double-integer-binary-casts-deprecated

Non-canonical cast names (boolean), (integer), (double), and (binary)
have been deprecated, use (bool), (int), (float), and (string) respectively.

Author: vmcj

webapp/src/Controller/Jury/RejudgingController.php

@@ -126,7 +126,7 @@ public function indexAction(): Response
                 $status = $rejudging->getValid() ? 'applied' : 'canceled';
                 $sort_order = 2;
             } elseif ($todo > 0) {
-                $perc   = (int)(100 * ((double)$done / (double)($done + $todo)));
+                $perc   = (int)(100 * ((float)$done / (float)($done + $todo)));
                 $status = sprintf("%d%% done", $perc);
                 $sort_order = 0;
             } else {