tuned script
authorhaftmann
Thu Jul 08 16:17:44 2010 +0200 (2010-07-08)
changeset 37741763feb2abb0d
parent 37740 9bb4a74cff4e
child 37742 d8e7f473c3a1
tuned script
Admin/check_ml_headers
     1.1 --- a/Admin/check_ml_headers	Thu Jul 08 09:36:23 2010 +0200
     1.2 +++ b/Admin/check_ml_headers	Thu Jul 08 16:17:44 2010 +0200
     1.3 @@ -1,14 +1,14 @@
     1.4  #!/usr/bin/env bash
     1.5  #
     1.6 -# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
     1.7 +# check_ml_headers - check headers of *.ML files in distribution for inconsistencies
     1.8  #
     1.9  # requires some GNU tools
    1.10  #
    1.11  
    1.12 -ONLY_FILENAMES=1
    1.13 +ONLY_FILENAMES=""
    1.14  if [ "$1" == "-o" ]
    1.15  then
    1.16 -  ONLY_FILENAMES=""
    1.17 +  ONLY_FILENAMES=1
    1.18  fi
    1.19  
    1.20  REPORT_EMPTY=""
    1.21 @@ -25,9 +25,9 @@
    1.22    FILELOC="${LOC:${#ISABELLE_SRC}}"
    1.23    if [ "$TITLE" != "$FILELOC" ]
    1.24    then
    1.25 -    if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
    1.26 +    if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ]
    1.27      then
    1.28 -      if [ -n "$ONLY_FILENAMES" ]
    1.29 +      if [ -z "$ONLY_FILENAMES" ]
    1.30        then
    1.31          echo "Inconsistency in $LOC: $TITLE"
    1.32        else