1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/lib/Tools/mkfifo Thu Aug 28 19:31:13 2008 +0200
1.3 @@ -0,0 +1,34 @@
1.4 +#!/usr/bin/env bash
1.5 +#
1.6 +# $Id$
1.7 +# Author: Makarius
1.8 +#
1.9 +# DESCRIPTION: create named pipe
1.10 +
1.11 +
1.12 +PRG="$(basename "$0")"
1.13 +
1.14 +function usage()
1.15 +{
1.16 + echo
1.17 + echo "Usage: $PRG"
1.18 + echo
1.19 + echo " Create a temporary named pipe and return its name."
1.20 + echo
1.21 + exit 1
1.22 +}
1.23 +
1.24 +function fail()
1.25 +{
1.26 + echo "$1" >&2
1.27 + exit 2
1.28 +}
1.29 +
1.30 +
1.31 +## main
1.32 +
1.33 +[ "$#" != 0 ] && usage
1.34 +
1.35 +FIFO="${ISABELLE_TMP_PREFIX}-fifo$$"
1.36 +mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO"
1.37 +echo "$FIFO"