more uniform make_polyml_gmp vs. make_polyml;
--- a/src/Pure/Admin/component_polyml.scala Sat Apr 12 17:12:51 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala Sat Apr 12 17:24:09 2025 +0200
@@ -84,8 +84,8 @@
"[ -f Makefile ] && make distclean",
"./configure --disable-static --enable-shared --enable-cxx" +
" --build=" + platform_arch + "-" + platform_os +
- " --prefix=" + Bash.string(platform_context.standard_path(target_dir)) +
- if_proper(options, " " + Bash.strings(options)),
+ """ --prefix="$PWD/target" """ + Bash.strings(options),
+ "rm -rf target",
"make",
"make check",
"make install")