--- 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"