diff -r 9d75d65a1a7a -r 386576a416ea lib/Tools/mkfifo
--- a/lib/Tools/mkfifo	Mon Sep 20 11:55:36 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: create named pipe
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG"
-  echo
-  echo "  Create a temporary named pipe and return its name."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## main
-
-[ "$#" != 0 ] && usage
-
-#FIXME potential race condition wrt. future processes with same pid
-FIFO="/tmp/isabelle-fifo$$"
-
-mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO"
-echo "$FIFO"