Admin/cronjob/main
changeset 73705 ac07f6be27ea
parent 64498 bb29e6849a28
child 74034 d6ae3a7d9cb0
--- a/Admin/cronjob/main	Sun May 16 19:37:15 2021 +0200
+++ b/Admin/cronjob/main	Mon May 17 13:57:19 2021 +1000
@@ -2,6 +2,7 @@
 #
 # DESCRIPTION: start the main Isabelle cronjob
 
+unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
 source "$HOME/.bashrc"