changeset 74635 | b179891dd357 |
parent 73672 | 70d3c7009a65 |
child 75202 | 4fdde010086f |
--- a/src/Pure/Admin/build_polyml.scala Sat Oct 30 11:59:41 2021 +0200 +++ b/src/Pure/Admin/build_polyml.scala Sat Oct 30 12:03:43 2021 +0200 @@ -89,7 +89,7 @@ { ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """ rm -rf target - make compiler && make compiler && make install + make && make install } || { echo "Build failed" >&2; exit 2; } """, redirect = true, echo = true).check