src/Pure/ROOT.ML
changeset 60962 faa452d8e265
parent 60959 3565c9f407ec
child 61261 ddb2da7cb2e4
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 17 23:16:03 2015 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Aug 17 23:45:12 2015 +0200
     1.3 @@ -115,9 +115,9 @@
     1.4  if Multithreading.available then ()
     1.5  else use "Concurrent/single_assignment_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 +if not Multithreading.available then use "Concurrent/bash_sequential.ML"
    1.11 +else if ML_System.platform_is_windows then use "Concurrent/bash_windows.ML"
    1.12 +else use "Concurrent/bash.ML";
    1.13  
    1.14  use "Concurrent/par_exn.ML";
    1.15  use "Concurrent/task_queue.ML";