# HG changeset patch # User wenzelm # Date 1343128926 -7200 # Node ID 5b9d79c6323b0c0f8209abd7ed4642a172ce9782 # Parent 8f10b1f6c992a4f837c894f54a1cde13b9e19892 tuned messages (cf. isabelle makeall); diff -r 8f10b1f6c992 -r 5b9d79c6323b lib/Tools/build --- a/lib/Tools/build Tue Jul 24 13:11:50 2012 +0200 +++ b/lib/Tools/build Tue Jul 24 13:22:06 2012 +0200 @@ -9,6 +9,17 @@ PRG="$(basename "$0")" +function show_settings() +{ + local PREFIX="$1" + echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" + echo + echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\"" + echo "${PREFIX}ML_HOME=\"$ML_HOME\"" + echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\"" + echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\"" +} + function usage() { echo @@ -26,12 +37,7 @@ echo " -v verbose" echo echo " Build and manage Isabelle sessions, depending on implicit" - echo " ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" - echo - echo " ML_PLATFORM=\"$ML_PLATFORM\"" - echo " ML_HOME=\"$ML_HOME\"" - echo " ML_SYSTEM=\"$ML_SYSTEM\"" - echo " ML_OPTIONS=\"$ML_OPTIONS\"" + show_settings " " echo exit 1 } @@ -105,6 +111,26 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } -exec "$ISABELLE_TOOL" java isabelle.Build \ +if [ "$NO_BUILD" = false ]; then + echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" + + if [ "$VERBOSE" = true ]; then + show_settings "" + echo + fi + . "$ISABELLE_HOME/lib/scripts/timestart.bash" +fi + +"$ISABELLE_TOOL" java isabelle.Build \ "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \ "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" +RC="$?" + +if [ "$NO_BUILD" = false ]; then + echo -n "Finished at "; date + + . "$ISABELLE_HOME/lib/scripts/timestop.bash" + echo "$TIMES_REPORT" +fi + +exit "$RC"