--- a/lib/Tools/mkfifo Sun Sep 19 22:40:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: create named pipe
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [SUFFIX]"
- echo
- echo " Create a temporary named pipe and return its name."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## main
-
-SUFFIX=""
-[ "$#" != 0 ] && { SUFFIX="-$1"; shift; }
-
-[ "$#" != 0 ] && usage
-
-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"