# HG changeset patch
# User wenzelm
# Date 1284831507 -7200
# Node ID 7ed922d158272f73cbb89ee3e811364e38cdc3b0
# Parent  bad14b7d0520528d8adbb54b25303d9ee66709cd
mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default;

diff -r bad14b7d0520 -r 7ed922d15827 lib/Tools/mkfifo
--- 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"