Admin/setup
changeset 73760 a35b2ee3148f
parent 73759 c259c7a42ac3
child 73761 d34033a93711
equal deleted inserted replaced
73759:c259c7a42ac3 73760:a35b2ee3148f
   146   export HGPLAIN=
   146   export HGPLAIN=
   147 
   147 
   148   "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
   148   "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
   149 
   149 
   150   #Atomic exec: avoid inplace update of running script!
   150   #Atomic exec: avoid inplace update of running script!
   151   export CLEAN REV ISABELLE_REPOS BUILD_OPTIONS
   151   export CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
   152   exec bash -c '
   152   exec bash -c '
   153     set -e
   153     set -e
   154     "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
   154     "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
   155     "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
   155     "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
   156     "$ISABELLE_HOME/bin/isabelle" components -a
   156     "$ISABELLE_HOME/bin/isabelle" components -a