1.1 --- a/lib/Tools/build Mon Jul 30 13:44:40 2012 +0200
1.2 +++ b/lib/Tools/build Mon Jul 30 13:48:56 2012 +0200
1.3 @@ -115,13 +115,11 @@
1.4
1.5 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
1.6
1.7 -if [ "$NO_BUILD" = false ]; then
1.8 +if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
1.9 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
1.10
1.11 - if [ "$VERBOSE" = true ]; then
1.12 - show_settings ""
1.13 - echo
1.14 - fi
1.15 + show_settings ""
1.16 + echo
1.17 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
1.18 fi
1.19
1.20 @@ -131,7 +129,7 @@
1.21 "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
1.22 RC="$?"
1.23
1.24 -if [ "$NO_BUILD" = false ]; then
1.25 +if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
1.26 echo -n "Finished at "; date
1.27
1.28 . "$ISABELLE_HOME/lib/scripts/timestop.bash"