author | wenzelm |
Mon, 19 Sep 2011 14:40:38 +0200 | |
changeset 45868 | fd3a36e48b09 |
parent 45867 | 6f27ecf2a951 |
child 45869 | 33aa6da101d8 |
lib/Tools/display | file | annotate | diff | comparison | revisions |
1.1 --- a/lib/Tools/display Mon Sep 19 14:31:20 2011 +0200 1.2 +++ b/lib/Tools/display Mon Sep 19 14:40:38 2011 +0200 1.3 @@ -74,7 +74,6 @@ 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 rm -f "$PRIVATE_FILE" 1.9 else 1.10 exec $VIEWER "$FILE"