proper export;
authorwenzelm
Sun, 28 Mar 2021 12:02:20 +0200
changeset 73760 a35b2ee3148f
parent 73759 c259c7a42ac3
child 73761 d34033a93711
proper export;
Admin/setup
--- a/Admin/setup	Sun Mar 28 11:59:30 2021 +0200
+++ b/Admin/setup	Sun Mar 28 12:02:20 2021 +0200
@@ -148,7 +148,7 @@
   "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
 
   #Atomic exec: avoid inplace update of running script!
-  export CLEAN REV ISABELLE_REPOS BUILD_OPTIONS
+  export CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
   exec bash -c '
     set -e
     "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"