src/Pure/ROOT.ML
changeset 43847 529159f81d06
parent 43795 ca5896a836ba
child 43850 7f2cbc713344
     1.1 --- a/src/Pure/ROOT.ML	Sat Jul 16 18:11:14 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sat Jul 16 18:20:02 2011 +0200
     1.3 @@ -79,11 +79,7 @@
     1.4  if Multithreading.available
     1.5  then use "Concurrent/bash.ML"
     1.6  else use "Concurrent/bash_sequential.ML";
     1.7 -
     1.8 -fun bash s =
     1.9 -  (case bash_output s of
    1.10 -    ("", rc) => rc
    1.11 -  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
    1.12 +use "Concurrent/bash_ops.ML";
    1.13  
    1.14  use "Concurrent/mailbox.ML";
    1.15  use "Concurrent/task_queue.ML";