| author | huffman | 
| Wed, 11 Feb 2009 11:22:42 -0800 | |
| changeset 29878 | 06efd6e731c6 | 
| parent 29143 | 72c960b2b83e | 
| child 38253 | 3d4e521014f7 | 
| permissions | -rwxr-xr-x | 
| 28047 | 1 | #!/usr/bin/env bash | 
| 2 | # | |
| 3 | # Author: Makarius | |
| 4 | # | |
| 5 | # DESCRIPTION: create named pipe | |
| 6 | ||
| 7 | ||
| 8 | PRG="$(basename "$0")" | |
| 9 | ||
| 10 | function usage() | |
| 11 | {
 | |
| 12 | echo | |
| 28650 | 13 | echo "Usage: isabelle $PRG" | 
| 28047 | 14 | echo | 
| 15 | echo " Create a temporary named pipe and return its name." | |
| 16 | echo | |
| 17 | exit 1 | |
| 18 | } | |
| 19 | ||
| 20 | function fail() | |
| 21 | {
 | |
| 22 | echo "$1" >&2 | |
| 23 | exit 2 | |
| 24 | } | |
| 25 | ||
| 26 | ||
| 27 | ## main | |
| 28 | ||
| 29 | [ "$#" != 0 ] && usage | |
| 30 | ||
| 28061 
5428435de53e
use hardwired /tmp -- fifo only work on local file-system;
 wenzelm parents: 
28047diff
changeset | 31 | FIFO="/tmp/isabelle-fifo$$" | 
| 28047 | 32 | mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO" | 
| 33 | echo "$FIFO" |