diff options
| author | Ralf Jung <post@ralfj.de> | 2022-11-27 13:20:44 +0100 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2022-11-27 13:20:44 +0100 |
| commit | b20efbd79f54cf5488f4b312db0ec64946234ec2 (patch) | |
| tree | db3dabd8c72529b0565a756c5134e98b061eb897 | |
| parent | 144b4859ad2c9fcee453f3a1000357e20ecad535 (diff) | |
| download | rust-b20efbd79f54cf5488f4b312db0ec64946234ec2.tar.gz rust-b20efbd79f54cf5488f4b312db0ec64946234ec2.zip | |
CI: fix begingroup printing
| -rwxr-xr-x | src/tools/miri/ci.sh | 2 |
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 } |