# HG changeset patch
# User wenzelm
# Date 904218821 -7200
# Node ID 8f1157817bb671f930c8a5e7d85ebd9ceb6e22df
# Parent  4325d853494ab11a1e0a1c46f2b57ef0e4a9ef8b
ISABELLE_USEDIR_OPTIONS="-i false";

diff -r 4325d853494a -r 8f1157817bb6 etc/settings
--- 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"
 
 
 ###