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