# HG changeset patch
# User wenzelm
# Date 1337506473 -7200
# Node ID 21c42b095c841d1a7508c143d6b6e98d95dbfa69
# Parent  9dcfcdbdb2ba27b953aac4e83883040bb9cc859b
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

diff -r 9dcfcdbdb2ba -r 21c42b095c84 lib/Tools/display
--- 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"