# HG changeset patch
# User wenzelm
# Date 1246572959 -7200
# Node ID d6f8f3bfe3292aadf2c19a856fefaef22b53857c
# Parent  f39825f8bfd34da7e0013ec0e3c5b45231cd0e68
allow reloading of settings within JVM process;

diff -r f39825f8bfd3 -r d6f8f3bfe329 Isabelle
--- a/Isabelle	Fri Jul 03 00:10:19 2009 +0200
+++ b/Isabelle	Fri Jul 03 00:15:59 2009 +0200
@@ -15,6 +15,8 @@
 ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
+unset ISABELLE_SETTINGS_PRESENT
+
 
 ## main