Admin/build
changeset 73705 ac07f6be27ea
parent 71367 91d5a8255c98
child 73987 fc363a3b690a
--- a/Admin/build	Sun May 16 19:37:15 2021 +0200
+++ b/Admin/build	Mon May 17 13:57:19 2021 +1000
@@ -5,6 +5,7 @@
 ## directory layout
 
 if [ -z "$ISABELLE_HOME" ]; then
+  unset CDPATH
   ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
   ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 fi