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