diff -r 3844037a8e2d -r 223a3de1222b lib/Tools/display
--- a/lib/Tools/display	Mon Nov 13 15:55:38 2006 +0100
+++ b/lib/Tools/display	Mon Nov 13 18:19:24 2006 +0100
@@ -75,7 +75,7 @@
   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
   $VIEWER "$PRIVATE_FILE"
-  sleep 5   ;try to avoid races
+  sleep 5   #try to avoid races
   rm -f "$PRIVATE_FILE"
 else
   exec $VIEWER "$FILE"