diff --git a/mps/INSTALL b/mps/INSTALL new file mode 120000 index 00000000000..e989720e22b --- /dev/null +++ b/mps/INSTALL @@ -0,0 +1 @@ +manual/build.txt \ No newline at end of file diff --git a/mps/README b/mps/README new file mode 120000 index 00000000000..0d79d56d9fb --- /dev/null +++ b/mps/README @@ -0,0 +1 @@ +readme.txt \ No newline at end of file