# HG changeset patch
# User wenzelm
# Date 1744471449 -7200
# Node ID 3b36c814b7f8bbbee32c26217e2f8a3e14d4594c
# Parent  537e81b823290fd78c73cab2422a335a157f0ca1
more uniform make_polyml_gmp vs. make_polyml;

diff -r 537e81b82329 -r 3b36c814b7f8 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")