author | wenzelm |
Wed, 18 Sep 2013 13:31:44 +0200 | |
changeset 53710 | 5ec27e55ddc2 |
parent 53709 | 84522727f9d3 |
child 53711 | 8ce7795256e1 |
src/Pure/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/ROOT.ML Wed Sep 18 13:18:51 2013 +0200 +++ b/src/Pure/ROOT.ML Wed Sep 18 13:31:44 2013 +0200 @@ -79,7 +79,7 @@ then use "ML/exn_trace_polyml-5.5.1.ML" else (); -if ML_System.name = "polyml-5.5.0" +if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1" then use "ML/ml_statistics_polyml-5.5.0.ML" else use "ML/ml_statistics_dummy.ML";