equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # 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 |
4 # |
4 # |
5 # requires some GNU tools |
5 # requires some GNU tools |
6 # |
6 # |
7 |
7 |
8 ONLY_FILENAMES=1 |
8 ONLY_FILENAMES="" |
9 if [ "$1" == "-o" ] |
9 if [ "$1" == "-o" ] |
10 then |
10 then |
11 ONLY_FILENAMES="" |
11 ONLY_FILENAMES=1 |
12 fi |
12 fi |
13 |
13 |
14 REPORT_EMPTY="" |
14 REPORT_EMPTY="" |
15 if [ "$2" == "-e" ] |
15 if [ "$2" == "-e" ] |
16 then |
16 then |
23 do |
23 do |
24 TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')" |
24 TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')" |
25 FILELOC="${LOC:${#ISABELLE_SRC}}" |
25 FILELOC="${LOC:${#ISABELLE_SRC}}" |
26 if [ "$TITLE" != "$FILELOC" ] |
26 if [ "$TITLE" != "$FILELOC" ] |
27 then |
27 then |
28 if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ] |
28 if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ] |
29 then |
29 then |
30 if [ -n "$ONLY_FILENAMES" ] |
30 if [ -z "$ONLY_FILENAMES" ] |
31 then |
31 then |
32 echo "Inconsistency in $LOC: $TITLE" |
32 echo "Inconsistency in $LOC: $TITLE" |
33 else |
33 else |
34 echo "$LOC" |
34 echo "$LOC" |
35 fi |
35 fi |