author | wenzelm |
Mon, 13 Nov 2006 18:19:24 +0100 | |
changeset 21342 | 223a3de1222b |
parent 21341 | 3844037a8e2d |
child 21343 | 320e136db6dc |
lib/Tools/display | file | annotate | diff | comparison | revisions |
--- 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"