src/Pure/ROOT.ML
changeset 41710 11ae688e4e30
parent 41228 e1fce873b814
child 41718 05514b09bb4b
     1.1 --- a/src/Pure/ROOT.ML	Fri Feb 04 21:52:36 2011 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Sat Feb 05 18:09:57 2011 +0100
     1.3 @@ -72,6 +72,10 @@
     1.4  if Multithreading.available then ()
     1.5  else use "Concurrent/synchronized_sequential.ML";
     1.6  
     1.7 +use "Concurrent/time_limit.ML";
     1.8 +if Multithreading.available then ()
     1.9 +else use "Concurrent/time_limit_dummy.ML";
    1.10 +
    1.11  if Multithreading.available
    1.12  then use "Concurrent/bash.ML"
    1.13  else use "Concurrent/bash_sequential.ML";