no "$id" header

mvorisek · mvorisek · commit 0ed4ec5de591 · 2022-09-22T12:11:15.000+02:00
diff --git a/run-tests.php b/run-tests.php
@@ -23,8 +23,6 @@
    +----------------------------------------------------------------------+
  */
 
-/* $Id$ */
-
 /* Temporary variables while this file is being refactored. */
 /** @var ?JUnit */
 $junit = null;
