# HG changeset patch
# User wenzelm
# Date 1285417019 -7200
# Node ID 6bb073e0385d2d6b8c74cbe64a54178163302ede
# Parent  625a3bc4417b3bf8d81aa0765d04f856e3597b61
tuned mk_fifo;

diff -r 625a3bc4417b -r 6bb073e0385d src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Sep 25 13:57:34 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Sep 25 14:16:59 2010 +0200
@@ -315,10 +315,10 @@
     val i = next_fifo()
     val script =
       "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$-" + i + "\"\n" +
-      "mkfifo -m 600 \"$FIFO\" || { echo \"Failed to create fifo: $FIFO\" >&2; exit 2; }\n" +
-      "echo -n \"$FIFO\"\n"
+      "echo -n \"$FIFO\"\n" +
+      "mkfifo -m 600 \"$FIFO\"\n"
     val (out, err, rc) = bash(script)
-    if (rc == 0) out else error(err)
+    if (rc == 0) out else error(err.trim)
   }
 
   def rm_fifo(fifo: String): Boolean =