From b824bb1158aadb8cae1d983968f44db10812785a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 20 Oct 2023 08:04:49 +0200 Subject: [PATCH] ignore deny lints in josh --- src/tools/miri/.github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tools/miri/.github/workflows/ci.yml b/src/tools/miri/.github/workflows/ci.yml index a5c5cb0d6cc..67b48a3742d 100644 --- a/src/tools/miri/.github/workflows/ci.yml +++ b/src/tools/miri/.github/workflows/ci.yml @@ -188,7 +188,7 @@ jobs: with: fetch-depth: 256 # get a bit more of the history - name: install josh-proxy - run: cargo +stable install josh-proxy --git https://github.com/josh-project/josh --tag r22.12.06 + run: RUSTFLAGS="--cap-lints warn" cargo +stable install josh-proxy --git https://github.com/josh-project/josh --tag r22.12.06 - name: setup bot git name and email run: | git config --global user.name 'The Miri Conjob Bot'