# 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