diff --git a/mps/tool/testopendylan b/mps/tool/testopendylan index 9c18938ef1e..a8aee4a0025 100755 --- a/mps/tool/testopendylan +++ b/mps/tool/testopendylan @@ -104,7 +104,7 @@ if [ -f "$REPO/Makefile" ]; then else ( cd -- "$REPO" && ./autogen.sh && - ./configure --with-mps="$MPS" --prefix="$PREFIX" + ./configure --with-gc=mps --with-gc-path="$MPS" --prefix="$PREFIX" ) fi ( cd -- "$REPO" && @@ -128,6 +128,9 @@ else ( # # 2014-03-20 GDR Created based on [WELCOME]. # +# 2014-04-14 GDR Updated configure args based on revised build +# instructions [WELCOME]. +# # # C. COPYRIGHT AND LICENCE #