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