src/Pure/ROOT.ML
changeset 40748 591b6778d076
parent 40743 b07a0dbc8a38
child 41228 e1fce873b814
     1.1 --- a/src/Pure/ROOT.ML	Sat Nov 27 16:27:52 2010 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Sat Nov 27 16:29:53 2010 +0100
     1.3 @@ -72,6 +72,15 @@
     1.4  if Multithreading.available then ()
     1.5  else use "Concurrent/synchronized_sequential.ML";
     1.6  
     1.7 +if Multithreading.available
     1.8 +then use "Concurrent/bash.ML"
     1.9 +else use "Concurrent/bash_sequential.ML";
    1.10 +
    1.11 +fun bash s =
    1.12 +  (case bash_output s of
    1.13 +    ("", rc) => rc
    1.14 +  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
    1.15 +
    1.16  use "Concurrent/mailbox.ML";
    1.17  use "Concurrent/task_queue.ML";
    1.18  use "Concurrent/future.ML";