changeset 47884 | 21c42b095c84 |
parent 44987 | fd3a36e48b09 |
child 50197 | b385d134926d |
--- a/lib/Tools/display Thu May 17 16:04:39 2012 +0200 +++ b/lib/Tools/display Sun May 20 11:34:33 2012 +0200 @@ -74,6 +74,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 rm -f "$PRIVATE_FILE" else exec $VIEWER "$FILE"