# HG changeset patch # User haftmann # Date 1190093769 -7200 # Node ID 6ab574864cd4b8707fe76ef7e6eb39869363316d # Parent bc484b2671fd08cd6f099838b7e57b4cc9e68e16 added script checking for consistency of ML file header diff -r bc484b2671fd -r 6ab574864cd4 Admin/check_ml_headers --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/check_ml_headers Tue Sep 18 07:36:09 2007 +0200 @@ -0,0 +1,40 @@ +#!/usr/bin/env bash +# +# $Id$ +# +# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies +# +# requires some GNU tools +# + +ONLY_FILENAMES=1 +if [ "$1" == "-o" ] +then + ONLY_FILENAMES="" +fi + +REPORT_EMPTY="" +if [ "$2" == "-e" ] +then + REPORT_EMPTY=1 +fi + +ISABELLE_SRC="$(isatool getenv -b ISABELLE_HOME)/src/" + +for LOC in $(find "$ISABELLE_SRC" -name "*.ML") +do + TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')" + FILELOC="${LOC:${#ISABELLE_SRC}}" + if [ "$TITLE" != "$FILELOC" ] + then + if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ] + then + if [ -n "$ONLY_FILENAMES" ] + then + echo "Inconsistency in $LOC: $TITLE" + else + echo "$LOC" + fi + fi + fi +done