Admin/check_ml_headers
changeset 28504 7ad7d7d6df47
parent 24618 6ab574864cd4
child 36859 51af1657263b
equal deleted inserted replaced
28503:a30b7169fdd1 28504:7ad7d7d6df47
    17 if [ "$2" == "-e" ]
    17 if [ "$2" == "-e" ]
    18 then
    18 then
    19   REPORT_EMPTY=1
    19   REPORT_EMPTY=1
    20 fi
    20 fi
    21 
    21 
    22 ISABELLE_SRC="$(isatool getenv -b ISABELLE_HOME)/src/"
    22 ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
    23 
    23 
    24 for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
    24 for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
    25 do
    25 do
    26   TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
    26   TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
    27   FILELOC="${LOC:${#ISABELLE_SRC}}"
    27   FILELOC="${LOC:${#ISABELLE_SRC}}"