lib/scripts/fileident
author bulwahn
Wed, 24 Mar 2010 17:40:43 +0100
changeset 35950 791ce568d40a
parent 29145 b1c6f4563df7
permissions -rwxr-xr-x
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23838
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     2
#
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     3
# fileident --- produce file identification based
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     4
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     5
FILE="$1"
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     6
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     7
if [ -n "$ISABELLE_FILE_IDENT" -a -f "$FILE" -a -r "$FILE" ]
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     8
then
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
     9
  ID=$(cat "$FILE" | $ISABELLE_FILE_IDENT | cut -d " " -f 1) && echo -n "$ID"
d2a8f1544bc9 fileident --- produce file identification based;
wenzelm
parents:
diff changeset
    10
fi