tuned;

--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 11 16:49:59 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 11 16:52:26 2016 +0100
@@ -9,6 +9,8 @@
 
 object Build_PolyML
 {
+  /** build_polyml **/
+
   sealed case class Platform_Info(
     options: List[String] = Nil,
     options_multilib: List[String] = Nil,
@@ -143,6 +145,7 @@
   }
 
 
+
   /** command line entry point **/
 
   def main(args: Array[String])