| author | wenzelm |
| Sat, 04 Oct 2008 16:05:09 +0200 | |
| changeset 28500 | 4b79e5d3d0aa |
| parent 28063 | 3533485fc7b8 |
| child 28650 | a7ba12e0d3b7 |
| permissions | -rwxr-xr-x |
| 28063 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# $Id$ |
|
4 |
# Author: Makarius |
|
5 |
# |
|
6 |
# DESCRIPTION: remove named pipe |
|
7 |
||
8 |
||
9 |
PRG="$(basename "$0")" |
|
10 |
||
11 |
function usage() |
|
12 |
{
|
|
13 |
echo |
|
14 |
echo "Usage: $PRG NAME" |
|
15 |
echo |
|
16 |
echo " Remove an unused named pipe, after producing dummy output" |
|
17 |
echo " to unblock the reader (blocks if no reader present)." |
|
18 |
echo |
|
19 |
exit 1 |
|
20 |
} |
|
21 |
||
22 |
||
23 |
## main |
|
24 |
||
25 |
[ "$#" != 1 ] && usage |
|
26 |
FIFO="$1"; shift |
|
27 |
||
28 |
if [ -p "$FIFO" ]; then |
|
29 |
echo -n "" >"$FIFO" && rm -f "$FIFO" |
|
30 |
fi |