lib/scripts/fileident
author haftmann
Wed, 01 Sep 2010 11:09:50 +0200
changeset 38968 e55deaa22fff
parent 29145 b1c6f4563df7
permissions -rwxr-xr-x
do not print object frame around Scala includes -- this is in the responsibility of the user
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