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