lib/scripts/fileident
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40915 a4c956d1f91f
parent 29145 b1c6f4563df7
permissions -rwxr-xr-x
declaring quickcheck testers as default after their setup
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