1 files changed, 1 insertions, 1 deletions
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
 }