Admin/Isabelle_app/build
changeset 73705 ac07f6be27ea
parent 73192 e7437085e589
--- a/Admin/Isabelle_app/build	Sun May 16 19:37:15 2021 +0200
+++ b/Admin/Isabelle_app/build	Mon May 17 13:57:19 2021 +1000
@@ -2,6 +2,7 @@
 
 set -e
 
+unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 cd "$THIS"