lib/scripts/fileident
author wenzelm
Thu May 20 20:20:52 2010 +0200 (2010-05-20)
changeset 37012 106c56e916f8
parent 29145 b1c6f4563df7
permissions -rwxr-xr-x
enable shell script editor mode;
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