# HG changeset patch
# User wenzelm
# Date 1158599562 -7200
# Node ID f78dfa306918cc297a421292a0e3b5c17b279dd8
# Parent  c315ba088073d1c84392647656953f993b233a65
PRIVATE_FILE: slightly more robust way to create and dispose;

diff -r c315ba088073 -r f78dfa306918 lib/Tools/display
--- a/lib/Tools/display	Mon Sep 18 19:12:41 2006 +0200
+++ b/lib/Tools/display	Mon Sep 18 19:12:42 2006 +0200
@@ -72,11 +72,11 @@
 esac
 
 if [ -n "$CLEAN" ]; then
-  PRIVATE_FILE="$ISABELLE_TMP/$$"$(basename "$FILE")
+  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"
 fi
-