author | wenzelm |
Sun, 20 May 2012 11:34:33 +0200 | |
changeset 48755 | 21c42b095c84 |
parent 48754 | 9dcfcdbdb2ba |
child 48756 | 7443906996a8 |
child 48900 | b987aa8b9310 |
lib/Tools/display | file | annotate | diff | comparison | revisions |
1.1 --- a/lib/Tools/display Thu May 17 16:04:39 2012 +0200 1.2 +++ b/lib/Tools/display Sun May 20 11:34:33 2012 +0200 1.3 @@ -74,6 +74,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 rm -f "$PRIVATE_FILE" 1.9 else 1.10 exec $VIEWER "$FILE"