use hardwired /tmp -- fifo only work on local file-system;
authorwenzelm
Fri Aug 29 20:36:05 2008 +0200 (2008-08-29)
changeset 280615428435de53e
parent 28060 1ee2d3bc25db
child 28062 f454a20c1ab1
use hardwired /tmp -- fifo only work on local file-system;
lib/Tools/mkfifo
     1.1 --- a/lib/Tools/mkfifo	Fri Aug 29 08:14:59 2008 +0200
     1.2 +++ b/lib/Tools/mkfifo	Fri Aug 29 20:36:05 2008 +0200
     1.3 @@ -29,6 +29,6 @@
     1.4  
     1.5  [ "$#" != 0 ] && usage
     1.6  
     1.7 -FIFO="${ISABELLE_TMP_PREFIX}-fifo$$"
     1.8 +FIFO="/tmp/isabelle-fifo$$"
     1.9  mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO"
    1.10  echo "$FIFO"