Auto merge of rust-lang#2700 - RalfJung:begingroup, r=RalfJung

CI: fix begingroup printing
RalfJung · Nov 27, 2022 · 5a14c5a · 5a14c5a
2 parents 144b485 + b20efbd
commit 5a14c5a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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
 }