diff -r b91b1ebfc8a0 -r d7e0315fe423 Admin/polyml/settings --- a/Admin/polyml/settings Mon Nov 23 16:57:01 2015 +0100 +++ b/Admin/polyml/settings Mon Nov 23 17:56:11 2015 +0100 @@ -41,7 +41,7 @@ # ML settings - ML_SYSTEM=polyml-5.5.3 + ML_SYSTEM=polyml-5.6 ML_PLATFORM="$PLATFORM" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_SOURCES="$POLYML_HOME/src"