From b20efbd79f54cf5488f4b312db0ec64946234ec2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sun, 27 Nov 2022 13:20:44 +0100
Subject: [PATCH] CI: fix begingroup printing

---
 src/tools/miri/ci.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/tools/miri/ci.sh b/src/tools/miri/ci.sh
index e528be8b037..402b07df6cd 100755
--- a/src/tools/miri/ci.sh
+++ b/src/tools/miri/ci.sh
@@ -2,7 +2,7 @@
 set -euo pipefail
 
 function begingroup {
-  echo "::group::$1"
+  echo "::group::$@"
   set -x
 }