# 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" ###