lib/Tools/browser
changeset 58639 1df53737c59b
parent 57082 2c1c8b38e3f0
child 61294 2d3d26e9b191
--- a/lib/Tools/browser	Thu Oct 09 11:00:15 2014 +0200
+++ b/lib/Tools/browser	Thu Oct 09 11:15:03 2014 +0200
@@ -70,7 +70,7 @@
 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
 
 if [ -n "$GRAPHFILE" ]; then
-  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
+  PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
   if [ -n "$CLEAN" ]; then
     mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
   else