| changeset 28061 | 5428435de53e |
| parent 28047 | 8dcf4349cf6f |
| child 28650 | a7ba12e0d3b7 |
| 28060:1ee2d3bc25db | 28061:5428435de53e |
|---|---|
27 |
27 |
28 ## main |
28 ## main |
29 |
29 |
30 [ "$#" != 0 ] && usage |
30 [ "$#" != 0 ] && usage |
31 |
31 |
32 FIFO="${ISABELLE_TMP_PREFIX}-fifo$$" |
32 FIFO="/tmp/isabelle-fifo$$" |
33 mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO" |
33 mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO" |
34 echo "$FIFO" |
34 echo "$FIFO" |