lib/Tools/rmfifo
author wenzelm
Thu, 04 Jun 2009 17:31:38 +0200
changeset 31427 5a07cc86675d
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
reraise exceptions to preserve original position (ML system specific);

#!/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