23838
|
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
|