| changeset 61715 | 5dc95d957569 |
| parent 61669 | 27ca6147e3b3 |
| child 61794 | 4c232a2ddeab |
--- a/src/Pure/ROOT.ML Fri Nov 20 15:54:46 2015 +0000 +++ b/src/Pure/ROOT.ML Fri Nov 20 21:52:05 2015 +0100 @@ -106,6 +106,7 @@ orelse ML_System.name = "polyml-5.5.1" orelse ML_System.name = "polyml-5.5.2" orelse ML_System.name = "polyml-5.5.3" + orelse ML_System.name = "polyml-5.6" then use "ML/ml_statistics_polyml-5.5.0.ML" else use "ML/ml_statistics_dummy.ML";