# HG changeset patch
# User wenzelm
# Date 1163438364 -3600
# Node ID 223a3de1222ba47fc6e702561e7eb7268734db48
# Parent  3844037a8e2d24a47b5c2af4e8200d1aace90bba
fixed comment -- oops;

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"