# HG changeset patch
# User wenzelm
# Date 1354713227 -3600
# Node ID ce2796981c0c6847c218c41e46972c7a09fb636b
# Parent  2f8dc9e65401b7c27125faaa6739141d3d754ca1
tuned;

diff -r 2f8dc9e65401 -r ce2796981c0c lib/Tools/build
--- a/lib/Tools/build	Wed Dec 05 12:22:55 2012 +0100
+++ b/lib/Tools/build	Wed Dec 05 14:13:47 2012 +0100
@@ -148,7 +148,6 @@
 
 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   echo -n "Finished at "; date
-
 fi
 
 . "$ISABELLE_HOME/lib/scripts/timestop.bash"