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;
wenzelm@23838
     1
#!/usr/bin/env bash
wenzelm@23838
     2
#
wenzelm@23838
     3
# fileident --- produce file identification based
wenzelm@23838
     4
wenzelm@23838
     5
FILE="$1"
wenzelm@23838
     6
wenzelm@23838
     7
if [ -n "$ISABELLE_FILE_IDENT" -a -f "$FILE" -a -r "$FILE" ]
wenzelm@23838
     8
then
wenzelm@23838
     9
  ID=$(cat "$FILE" | $ISABELLE_FILE_IDENT | cut -d " " -f 1) && echo -n "$ID"
wenzelm@23838
    10
fi