diff -r b376f53bcc18 -r bad14b7d0520 lib/Tools/mkfifo
--- a/lib/Tools/mkfifo	Sat Sep 18 17:14:47 2010 +0200
+++ b/lib/Tools/mkfifo	Sat Sep 18 17:39:23 2010 +0200
@@ -10,7 +10,7 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG"
+  echo "Usage: isabelle $PRG [SUFFIX]"
   echo
   echo "  Create a temporary named pipe and return its name."
   echo
@@ -26,10 +26,12 @@
 
 ## main
 
+SUFFIX=""
+[ "$#" != 0 ] && { SUFFIX="-$1"; shift; }
+
 [ "$#" != 0 ] && usage
 
-#FIXME potential race condition wrt. future processes with same pid
-FIFO="/tmp/isabelle-fifo$$"
+FIFO="/tmp/isabelle-fifo${PPID}${SUFFIX}"
 
 mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO"
 echo "$FIFO"