lib/Tools/rmfifo
author wenzelm
Wed, 25 Mar 2009 16:54:49 +0100
changeset 30718 15041c7e51e4
parent 29143 72c960b2b83e
permissions -rwxr-xr-x
Proofterm.approximate_proof_body;

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