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