etc/settings
changeset 5387 8f1157817bb6
parent 4708 580bf0f3ef79
child 5659 e2a2be6089b4
     1.1 --- a/etc/settings	Thu Aug 27 13:52:46 1998 +0200
     1.2 +++ b/etc/settings	Thu Aug 27 13:53:41 1998 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  ### Compilation options
     1.5  ###
     1.6  
     1.7 -ISABELLE_USEDIR_OPTIONS=""
     1.8 +ISABELLE_USEDIR_OPTIONS="-i false"
     1.9  
    1.10  
    1.11  ###