# HG changeset patch
# User wenzelm
# Date 1648849867 -7200
# Node ID 45641af13418c1e02738d12f51b044778be3d636
# Parent  cd9f2d3820144e193775ce64641ebf01ca61cc60
clarified formatting, for the sake of scala3;

diff -r cd9f2d382014 -r 45641af13418 Admin/jenkins/build/ci_build_benchmark.scala
--- a/Admin/jenkins/build/ci_build_benchmark.scala	Fri Apr 01 23:26:19 2022 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Apr 01 23:51:07 2022 +0200
@@ -1,5 +1,4 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
 
   import isabelle._