src/Pure/Build/build_ci.scala

--- a/src/Pure/Build/build_ci.scala	Wed Jun 26 19:55:56 2024 +0200
+++ b/src/Pure/Build/build_ci.scala	Thu Jun 27 09:41:16 2024 +0200
@@ -112,6 +112,7 @@
     build_prefs: List[Options.Spec] = Nil,
     hook: Hook = none,
     extra_components: List[String] = Nil,
+    other_settings: List[String] = Nil,
     trigger: Trigger = On_Commit
   ) {
     override def toString: String = name