diff -r 8eac822dec6c -r 51af1657263b Admin/check_ml_headers --- a/Admin/check_ml_headers Wed May 12 13:52:34 2010 +0200 +++ b/Admin/check_ml_headers Wed May 12 13:54:49 2010 +0200 @@ -1,7 +1,5 @@ #!/usr/bin/env bash # -# $Id$ -# # check_ml_headers - check headers of *.ML files in Distribution for inconsistencies # # requires some GNU tools