# HG changeset patch
# User wenzelm
# Date 1184705487 -7200
# Node ID d2a8f1544bc987613ac85c38582c23696ced3958
# Parent  55b89b14d87198deff43377a0f569b42f008bb96
fileident --- produce file identification based;

diff -r 55b89b14d871 -r d2a8f1544bc9 lib/scripts/fileident
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/fileident	Tue Jul 17 22:51:27 2007 +0200
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+#
+# $Id$
+#
+# 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