# HG changeset patch
# User wenzelm
# Date 1220034965 -7200
# Node ID 5428435de53e7ac2f4cf2e66c073b92ceee9a391
# Parent  1ee2d3bc25db13793ff1737103cd3b43d7d97b76
use hardwired /tmp -- fifo only work on local file-system;

diff -r 1ee2d3bc25db -r 5428435de53e lib/Tools/mkfifo
--- a/lib/Tools/mkfifo	Fri Aug 29 08:14:59 2008 +0200
+++ b/lib/Tools/mkfifo	Fri Aug 29 20:36:05 2008 +0200
@@ -29,6 +29,6 @@
 
 [ "$#" != 0 ] && usage
 
-FIFO="${ISABELLE_TMP_PREFIX}-fifo$$"
+FIFO="/tmp/isabelle-fifo$$"
 mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO"
 echo "$FIFO"