# HG changeset patch
# User wenzelm
# Date 1750018478 -7200
# Node ID 2d99f3e24da49777c4946665329bbcdc09cf3d3d
# Parent  e1a8753eaad71284826aa8828d9e0681a7311082
support dynamic usage_text, after some options have been processed already;

diff -r e1a8753eaad7 -r 2d99f3e24da4 src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala	Sun Jun 15 15:19:03 2025 +0200
+++ b/src/Pure/System/getopts.scala	Sun Jun 15 22:14:38 2025 +0200
@@ -11,7 +11,7 @@
 
 
 object Getopts {
-  def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts = {
+  def apply(usage_text: => String, option_specs: (String, String => Unit)*): Getopts = {
     val options =
       option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
         case (m, (s, f)) =>
@@ -26,7 +26,7 @@
   }
 }
 
-class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)]) {
+class Getopts private(usage_text: => String, options: Map[Char, (Boolean, String => Unit)]) {
   def usage(): Nothing = {
     Output.writeln(usage_text, stdout = true)
     sys.exit(Process_Result.RC.error)