src/Pure/Concurrent/bash_ops.ML
changeset 43850 7f2cbc713344
parent 43849 00f4b305687d
child 43851 f7f8cf0a1536
     1.1 --- a/src/Pure/Concurrent/bash_ops.ML	Sat Jul 16 20:14:58 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,15 +0,0 @@
     1.4 -(*  Title:      Pure/Concurrent/bash_ops.ML
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Derived operations for bash_process.
     1.8 -*)
     1.9 -
    1.10 -fun bash_output s =
    1.11 -  let val {output, rc, ...} = bash_process s
    1.12 -  in (output, rc) end;
    1.13 -
    1.14 -fun bash s =
    1.15 -  (case bash_output s of
    1.16 -    ("", rc) => rc
    1.17 -  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
    1.18 -