obsolete (see also d547173212d2);
authorwenzelm
Sat, 28 Jan 2023 20:58:00 +0100
changeset 77129 c79da77d9e87
parent 77128 f40c36ab154d
child 77130 2b8cf3b94cde
obsolete (see also d547173212d2);
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jan 28 20:50:45 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Sat Jan 28 20:58:00 2023 +0100
@@ -114,7 +114,6 @@
     arch_64: Boolean = false,
     heap: Int = default_heap,
     max_heap: Option[Int] = None,
-    init_settings: List[String] = Nil,
     more_settings: List[String] = Nil,
     more_preferences: List[String] = Nil,
     verbose: Boolean = false,
@@ -197,7 +196,7 @@
         other_isabelle.init_components(
           components_base = components_base,
           catalogs = Components.optional_catalogs)
-      other_isabelle.init_settings(component_settings ::: init_settings)
+      other_isabelle.init_settings(component_settings)
       resolve_components()
       val ml_platform =
         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
@@ -415,7 +414,6 @@
       var more_preferences: List[String] = Nil
       var fresh = false
       var hostname = ""
-      var init_settings: List[String] = Nil
       var arch_64 = false
       var output_file = ""
       var ml_statistics_step = 1
@@ -475,7 +473,6 @@
         "e:" -> (arg => more_settings = more_settings ::: List(arg)),
         "f" -> (_ => fresh = true),
         "h:" -> (arg => hostname = arg),
-        "i:" -> (arg => init_settings = init_settings ::: List(arg)),
         "m:" ->
           {
             case "32" | "x86" => arch_64 = false
@@ -507,7 +504,7 @@
           fresh = fresh, hostname = hostname, multicore_base = multicore_base,
           multicore_list = multicore_list, arch_64 = arch_64,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
-          max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
+          max_heap = max_heap, more_settings = more_settings,
           more_preferences = more_preferences, verbose = verbose, build_tags = build_tags,
           build_args = build_args)