diff --git a/mps/index.html b/mps/index.html index 444dbe58289..5db4f9c9c5c 100644 --- a/mps/index.html +++ b/mps/index.html @@ -89,6 +89,14 @@ must therefore be branched and maintained in product versions.
example/
manual/