Admin/check_ml_headers
changeset 36859 51af1657263b
parent 28504 7ad7d7d6df47
child 37741 763feb2abb0d
     1.1 --- a/Admin/check_ml_headers	Wed May 12 13:52:34 2010 +0200
     1.2 +++ b/Admin/check_ml_headers	Wed May 12 13:54:49 2010 +0200
     1.3 @@ -1,7 +1,5 @@
     1.4  #!/usr/bin/env bash
     1.5  #
     1.6 -# $Id$
     1.7 -#
     1.8  # check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
     1.9  #
    1.10  # requires some GNU tools