ignore deny lints in josh
This commit is contained in:
parent
20fe485c57
commit
b824bb1158
1 changed files with 1 additions and 1 deletions
2
src/tools/miri/.github/workflows/ci.yml
vendored
2
src/tools/miri/.github/workflows/ci.yml
vendored
|
@ -188,7 +188,7 @@ jobs:
|
||||||
with:
|
with:
|
||||||
fetch-depth: 256 # get a bit more of the history
|
fetch-depth: 256 # get a bit more of the history
|
||||||
- name: install josh-proxy
|
- 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
|
- name: setup bot git name and email
|
||||||
run: |
|
run: |
|
||||||
git config --global user.name 'The Miri Conjob Bot'
|
git config --global user.name 'The Miri Conjob Bot'
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue