# HG changeset patch
# User wenzelm
# Date 1357998836 -3600
# Node ID 1465521b92a1ce3f732bbe656910e8f6f4762912
# Parent  777c6026ca934578ed41b1ef5ee08e6c9fbb7ffa
removed unused/non-portable bash_output_fifo;

diff -r 777c6026ca93 -r 1465521b92a1 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sat Jan 12 14:47:17 2013 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sat Jan 12 14:53:56 2013 +0100
@@ -14,7 +14,6 @@
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   val with_tmp_fifo: (Path.T -> 'a) -> 'a
-  val bash_output_fifo: string -> (Path.T -> 'a) -> 'a
   val bash_output: string -> string * int
   val bash: string -> int
 end;
@@ -99,15 +98,5 @@
         (_, 0) => f path
       | (out, _) => error (trim_line out)));
 
-(* FIXME blocks on Cygwin 1.7.x *)
-(* See also http://cygwin.com/ml/cygwin/2010-08/msg00459.html *)
-fun bash_output_fifo script f =
-  with_tmp_fifo (fn fifo =>
-    uninterruptible (fn restore_attributes => fn () =>
-      (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
-        {rc = 0, terminate, ...} =>
-          (restore_attributes f fifo handle exn => (terminate (); reraise exn))
-      | {out, ...} => error (trim_line out))) ());
-
 end;