more uniform make_polyml_gmp vs. make_polyml;
authorwenzelm
Sat, 12 Apr 2025 17:24:09 +0200
changeset 82492 3b36c814b7f8
parent 82491 537e81b82329
child 82493 5f98257dc912
more uniform make_polyml_gmp vs. make_polyml;
src/Pure/Admin/component_polyml.scala
--- 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")