# HG changeset patch
# User kleing
# Date 1046265978 -3600
# Node ID 4d50cf8ea3d7fd90475613e123651e3a9811f7ad
# Parent  f8dcb1d9ea6890ef3ca90b2558576bc1179da13c
== -> =

diff -r f8dcb1d9ea68 -r 4d50cf8ea3d7 lib/Tools/makeall
--- a/lib/Tools/makeall	Wed Feb 26 13:16:07 2003 +0100
+++ b/lib/Tools/makeall	Wed Feb 26 14:26:18 2003 +0100
@@ -49,4 +49,4 @@
 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
 echo "$ELAPSED total elapsed time"
 
-[ "$FAIL" == "" ] || fail "Logics ${FAIL}FAILED!"
+[ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"