--- a/lib/Tools/rmfifo Mon Sep 20 11:55:36 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: remove named pipe
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG NAME"
- echo
- echo " Remove an unused named pipe, after producing dummy output"
- echo " to unblock the reader (blocks if no reader present)."
- echo
- exit 1
-}
-
-
-## main
-
-[ "$#" != 1 ] && usage
-FIFO="$1"; shift
-
-if [ -p "$FIFO" ]; then
- echo -n "" >"$FIFO" && rm -f "$FIFO"
-fi