less verbosity;
authorwenzelm
Mon, 30 Jul 2012 13:48:56 +0200
changeset 49616655b08c2cd89
parent 49615 305ebcd9018a
child 49617 342ca8f3197b
less verbosity;
lib/Tools/build
     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"