# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1712909416 -7200
# Node ID 5af76462e3a5b1ed9b3b891392c36132fb74a57c
# Parent  c0d689c4fd151973954199cea481dfd4b9829e04
tuned;

diff -r c0d689c4fd15 -r 5af76462e3a5 src/Pure/Admin/ci_build.scala
--- a/src/Pure/Admin/ci_build.scala	Thu Apr 11 14:13:43 2024 +0200
+++ b/src/Pure/Admin/ci_build.scala	Fri Apr 12 10:10:16 2024 +0200
@@ -136,7 +136,7 @@
     Mercurial.repository(path).id()
 
   def print_section(title: String): Unit =
-    println(s"\n=== $title ===\n")
+    println("\n=== " + title + " ===\n")
 
   def ci_build(options: Options, job: Job): Unit = {
     val profile = job.profile
@@ -156,11 +156,12 @@
       with_documents(options, config).int.update("threads", profile.threads) +
         "parallel_proofs=1" + "system_heaps"
 
-    println(s"jobs = ${profile.jobs}, threads = ${profile.threads}, numa = ${profile.numa}")
+    println(
+      "jobs = " + profile.jobs + ", threads = " + profile.threads + ", numa = " + profile.numa)
 
     print_section("BUILD")
-    println(s"Build started at $formatted_time")
-    println(s"Isabelle id $isabelle_id")
+    println("Build started at " + formatted_time)
+    println("Isabelle id " + isabelle_id)
     val pre_result = config.pre_hook(options)
 
     print_section("LOG")
@@ -186,7 +187,7 @@
 
     val groups = results.sessions.map(results.info).flatMap(_.groups)
     for (group <- groups)
-      println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
+      println("Group " + group + ": " + compute_timing(results, Some(group)).message_resources)
 
     val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
     println("Overall: " + total_timing.message_resources)
@@ -195,10 +196,10 @@
       print_section("FAILED SESSIONS")
 
       for (name <- results.sessions) {
-        if (results.cancelled(name)) println(s"Session $name: CANCELLED")
+        if (results.cancelled(name)) println("Session " + name + ": CANCELLED")
         else {
           val result = results(name)
-          if (!result.ok) println(s"Session $name: FAILED ${ result.rc }")
+          if (!result.ok) println("Session " + name + ": FAILED " + result.rc)
         }
       }
     }