| author | wenzelm |
| Sat, 20 Dec 2008 11:55:34 +0100 | |
| changeset 29145 | b1c6f4563df7 |
| parent 23838 | d2a8f1544bc9 |
| permissions | -rwxr-xr-x |
| 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 |