lib/scripts/fileident
author wenzelm
Mon, 16 Feb 2009 21:23:33 +0100
changeset 29758 7a3b5bbed313
parent 29145 b1c6f4563df7
permissions -rwxr-xr-x
removed rudiments of glossary;
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