recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;
authorwenzelm
Thu, 30 Jul 2009 23:50:11 +0200
changeset 32294 d00238af17b6
parent 32293 e0b8da3fae4d
child 32295 400cc493d466
child 32297 3a4081abb3f7
child 32299 5f33ce0ed21f
child 32346 7d84fd5ef6ee
recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;
src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 30 23:37:53 2009 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 30 23:50:11 2009 +0200
@@ -17,7 +17,7 @@
 use "ML-Systems/polyml_common.ML";
 
 if ml_system = "polyml-5.2"
-then use "ML-Systems/thread_dummy.ML"
+then (use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML")
 else use "ML-Systems/multithreading_polyml.ML";
 
 val pointer_eq = PolyML.pointerEq;