--- 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"