lib/scripts/getsettings
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