equal
deleted
inserted
replaced
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 |
|