lib/scripts/fileident
author wenzelm
Sat Dec 20 11:55:34 2008 +0100 (2008-12-20)
changeset 29145 b1c6f4563df7
parent 23838 d2a8f1544bc9
permissions -rwxr-xr-x
removed Ids;
     1 #!/usr/bin/env bash
     2 #
     3 # fileident --- produce file identification based
     4 
     5 FILE="$1"
     6 
     7 if [ -n "$ISABELLE_FILE_IDENT" -a -f "$FILE" -a -r "$FILE" ]
     8 then
     9   ID=$(cat "$FILE" | $ISABELLE_FILE_IDENT | cut -d " " -f 1) && echo -n "$ID"
    10 fi