| changeset 41728 | 2837df4d1c7a |
| parent 41727 | ab3f6d76fb23 |
| parent 41718 | 05514b09bb4b |
| child 41729 | ae1a46cdb9cb |
--- a/src/Pure/Concurrent/time_limit_dummy.ML Tue Feb 08 16:10:10 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: Pure/Concurrent/time_limit_dummy.ML - Author: Makarius - -Execution with time limit -- dummy version. -*) - -structure TimeLimit: TIME_LIMIT = -struct - -exception TimeOut; - -fun timeLimit _ f x = (warning "No timeout support on this ML platform"; f x); - -end; -