fixed comment -- oops;
authorwenzelm
Mon, 13 Nov 2006 18:19:24 +0100
changeset 21342 223a3de1222b
parent 21341 3844037a8e2d
child 21343 320e136db6dc
fixed comment -- oops;
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"