changeset 76343 | 6a6f650cc5a2 |
parent 76326 | a39fa81929d4 |
child 77373 | eaf234b0c849 |
--- a/lib/scripts/getsettings Wed Oct 19 16:01:07 2022 +0200 +++ b/lib/scripts/getsettings Thu Oct 20 14:59:39 2022 +0200 @@ -41,7 +41,7 @@ ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")" ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" - unset CLASSPATH + export CLASSPATH="" else if [ -z "$USER_HOME" ]; then USER_HOME="$HOME" @@ -50,7 +50,7 @@ ISABELLE_ROOT="$ISABELLE_HOME" ISABELLE_CLASSPATH="$CLASSPATH" - unset CLASSPATH + export CLASSPATH="" fi #init cumulative settings