diff -r 7c7a59b76528 -r ac07f6be27ea Admin/Isabelle_app/build
--- 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"