try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09); Isabelle2012
authorwenzelm
Sun May 20 11:34:33 2012 +0200 (2012-05-20)
changeset 4788421c42b095c84
parent 47883 9dcfcdbdb2ba
child 47885 b987aa8b9310
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);
lib/Tools/display
     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"