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 }