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?*)