| changeset 18760 | 97aaecb84afe |
| parent 18504 | 6574d62fe76b |
| child 18814 | 1a904aebfef0 |
--- a/src/Pure/ML-Systems/polyml.ML Mon Jan 23 15:23:31 2006 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Mon Jan 23 17:29:52 2006 +0100 @@ -62,8 +62,12 @@ (* bounded time execution *) +(* FIXME proper implementation for Cygwin available? *) +fun interrupt_timeout time f x = + f x; + unless_cygwin - use "ML-Systems/polyml-time-limit.ML"; + use "ML-Systems/polyml-interrupt-timeout.ML"; (* prompts *)