mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default;
authorwenzelm
Sat, 18 Sep 2010 19:38:27 +0200
changeset 39521 7ed922d15827
parent 39520 bad14b7d0520
child 39522 01aade784da9
mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default;
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"