| changeset 23838 | d2a8f1544bc9 |
| child 29145 | b1c6f4563df7 |
| 23837:55b89b14d871 | 23838:d2a8f1544bc9 |
|---|---|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # fileident --- produce file identification based |
|
6 |
|
7 FILE="$1" |
|
8 |
|
9 if [ -n "$ISABELLE_FILE_IDENT" -a -f "$FILE" -a -r "$FILE" ] |
|
10 then |
|
11 ID=$(cat "$FILE" | $ISABELLE_FILE_IDENT | cut -d " " -f 1) && echo -n "$ID" |
|
12 fi |