lib/scripts/fileident
author noschinl
Wed, 23 Feb 2011 11:23:26 +0100
changeset 41827 98eda7ffde79
parent 29145 b1c6f4563df7
permissions -rwxr-xr-x
setup case_product attribute in HOL and FOL
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