diff -r 4e63872f3646 -r d4b3eea69371 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Thu Apr 10 13:09:53 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Thu Apr 10 13:15:57 2025 +0200
@@ -106,15 +106,15 @@
     }
 
     platform_context.bash(root,
-      info.setup + "\n" +
-      """
-        [ -f Makefile ] && make distclean
-        {
-          ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
-          rm -rf target
-          make && make install
-        } || { echo "Build failed" >&2; exit 2; }
-      """, redirect = true).check
+      Library.make_lines(
+        "set -e",
+        info.setup,
+        "[ -f Makefile ] && make distclean",
+        """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
+        "rm -rf target",
+        "make",
+        "make install"
+      ), redirect = true).check
 
 
     /* sha1 library */