Admin/check_ml_headers
changeset 36859 51af1657263b
parent 28504 7ad7d7d6df47
child 37741 763feb2abb0d
equal deleted inserted replaced
36858:8eac822dec6c 36859:51af1657263b
     1 #!/usr/bin/env bash
     1 #!/usr/bin/env bash
     2 #
       
     3 # $Id$
       
     4 #
     2 #
     5 # check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
     3 # check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
     6 #
     4 #
     7 # requires some GNU tools
     5 # requires some GNU tools
     8 #
     6 #