author | wenzelm |
Sat, 18 Sep 2010 19:38:27 +0200 | |
changeset 39521 | 7ed922d15827 |
parent 39520 | bad14b7d0520 |
child 39522 | 01aade784da9 |
lib/Tools/mkfifo | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/mkfifo Sat Sep 18 17:39:23 2010 +0200 +++ b/lib/Tools/mkfifo Sat Sep 18 19:38:27 2010 +0200 @@ -31,7 +31,10 @@ [ "$#" != 0 ] && usage -FIFO="/tmp/isabelle-fifo${PPID}${SUFFIX}" +ID="$PPID" +[ "$ID" = 0 -o "$ID" = 1 ] && ID="$$" # Cygwin workaround + +FIFO="/tmp/isabelle-fifo${ID}${SUFFIX}" mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO" echo "$FIFO"