diff -r fb94df4505a0 -r 703ea96b13c6 lib/scripts/fileident
--- a/lib/scripts/fileident	Sun Mar 13 20:21:24 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-#
-# fileident --- produce file identification based
-
-FILE="$1"
-
-if [ -n "$ISABELLE_FILE_IDENT" -a -f "$FILE" -a -r "$FILE" ]
-then
-  ID=$(cat "$FILE" | $ISABELLE_FILE_IDENT | cut -d " " -f 1) && echo -n "$ID"
-fi