# HG changeset patch
# User wenzelm
# Date 1220551583 -7200
# Node ID 03e5196b1559c52316a7b907c9a9d4aa943aef3a
# Parent  b82ddffe7429f08b65796cca91c03f1fd8e76ad7
check WRAPPER_OUTPUT node type;

diff -r b82ddffe7429 -r 03e5196b1559 bin/isabelle-process
--- a/bin/isabelle-process	Thu Sep 04 20:05:48 2008 +0200
+++ b/bin/isabelle-process	Thu Sep 04 20:06:23 2008 +0200
@@ -224,6 +224,7 @@
 
 NICE="nice"
 if [ -n "$WRAPPER_OUTPUT" ]; then
+  [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
   MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"