# HG changeset patch
# User wenzelm
# Date 1184705473 -7200
# Node ID 55b89b14d87198deff43377a0f569b42f008bb96
# Parent  c6094fe98dfd03a1d2b96508caaacf4a7a5cb620
added ISABELLE_FILE_IDENT (command line for source file identification);

diff -r c6094fe98dfd -r 55b89b14d871 etc/settings
--- a/etc/settings	Tue Jul 17 22:48:40 2007 +0200
+++ b/etc/settings	Tue Jul 17 22:51:13 2007 +0200
@@ -79,6 +79,13 @@
 HOL_USEDIR_OPTIONS=""
 #HOL_USEDIR_OPTIONS="-p 2"
 
+#Source file identification (default: full name + date stamp)
+ISABELLE_FILE_IDENT=""
+#ISABELLE_FILE_IDENT="md5"
+#ISABELLE_FILE_IDENT="md5sum"
+#ISABELLE_FILE_IDENT="sha1sum"
+#ISABELLE_FILE_IDENT="openssl dgst -sha1"
+
 
 ###
 ### Document preparation (cf. isatool latex/document)