--- 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"