CI: fix begingroup printing

diff --git a/src/tools/miri/ci.sh b/src/tools/miri/ci.sh
index e528be8b037af5b59decd8afdf528d44e2b4b020..402b07df6cde5085308e77c265efbb70d4b40fde 100755 (executable)
--- 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
 }