1.1 --- a/lib/Tools/display	Mon Nov 13 15:55:38 2006 +0100
     1.2 +++ b/lib/Tools/display	Mon Nov 13 18:19:24 2006 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4    PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
     1.5    mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
     1.6    $VIEWER "$PRIVATE_FILE"
     1.7 -  sleep 5   ;try to avoid races
     1.8 +  sleep 5   #try to avoid races
     1.9    rm -f "$PRIVATE_FILE"
    1.10  else
    1.11    exec $VIEWER "$FILE"