Fix more issues

DOMjudge · Jun 2, 2024 · 3695b7a · 3695b7a
1 parent d3214b3
commit 3695b7a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/docker/build.sh b/docker/build.sh
@@ -12,7 +12,7 @@ then
 	set -x
 	then
 		# Functions to annotate the Github actions logs
-		trace_on () { set -x }
+		trace_on () { set -x; }
 		trace_off () {
 			{ set +x; } 2>/dev/null
 		}
@@ -29,7 +29,7 @@ then
 
 		section_start () {
 			trace_off
-			section_start_internal
+			section_start_internal "$@"
 		}
 		section_end () {
 			trace_off