src/Pure/ML-Systems/mosml.ML
changeset 21280 b4aa7daa506b
parent 18760 97aaecb84afe
child 21298 6d2306b2376d
--- a/src/Pure/ML-Systems/mosml.ML	Thu Nov 09 23:40:19 2006 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Fri Nov 10 00:12:28 2006 +0100
@@ -97,10 +97,11 @@
 
 (* bounded time execution *)
 
-(* FIXME proper implementation available? *)
+(*dummy implementation*)
 fun interrupt_timeout time f x =
   f x;
 
+
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)