added ISABELLE_FILE_IDENT (command line for source file identification);
authorwenzelm
Tue, 17 Jul 2007 22:51:13 +0200
changeset 23837 55b89b14d871
parent 23836 c6094fe98dfd
child 23838 d2a8f1544bc9
added ISABELLE_FILE_IDENT (command line for source file identification);
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)