# HG changeset patch
# User wenzelm
# Date 1744283393 -7200
# Node ID 4e63872f36461f0935d0ce71db2408b78ca910ba
# Parent  1fa80133027d0bd04e9f1490e57524a872d93215
tuned comments;

diff -r 1fa80133027d -r 4e63872f3646 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Wed Apr 09 22:45:04 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Thu Apr 10 13:09:53 2025 +0200
@@ -10,7 +10,7 @@
 
 
 object Component_PolyML {
-  /** platform-specific build **/
+  /** platform information **/
 
   sealed case class Platform_Info(
     options: List[String] = Nil,
@@ -56,6 +56,10 @@
     }
   }
 
+
+
+  /** build stages **/
+
   def make_polyml(
     platform_context: Platform_Context,
     root: Path,