diff -r 9d75d65a1a7a -r 386576a416ea lib/Tools/rmfifo
--- 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