etc/settings
changeset 5387 8f1157817bb6
parent 4708 580bf0f3ef79
child 5659 e2a2be6089b4
--- a/etc/settings	Thu Aug 27 13:52:46 1998 +0200
+++ b/etc/settings	Thu Aug 27 13:53:41 1998 +0200
@@ -47,7 +47,7 @@
 ### Compilation options
 ###
 
-ISABELLE_USEDIR_OPTIONS=""
+ISABELLE_USEDIR_OPTIONS="-i false"
 
 
 ###