equal
deleted
inserted
replaced
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 |