diff -r 88a8911bb65d -r aa78df2e254b Admin/isatest-makeall
--- a/Admin/isatest-makeall	Fri May 09 14:15:50 2003 +0200
+++ b/Admin/isatest-makeall	Fri May 09 14:21:07 2003 +0200
@@ -119,7 +119,7 @@
         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
 
         # error log
-        echo "Test for platform ${SHORT}failed. Log file available at" >> $ERRORLOG
+        echo "Test for platform ${SHORT} failed. Log file available at" >> $ERRORLOG
         echo "$HOSTNAME:$TESTLOG" >> $ERRORLOG
         echo "[...]" >> $ERRORLOG
         tail -3 $L >> $ERRORLOG