user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

adjust josh pushing and remove ./miri toolchain updating the toolchain file

Browse source
This commit is contained in:
Ralf Jung 2022-11-15 18:52:06 +01:00
parent a046f62bb4
commit a47e431390
3 changed files with 40 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tools/miri/.github/workflows/ci.yml vendored
View file

@ -67,10 +67,10 @@ jobs:
shell: bash
run: |
if [[ ${{ github.event_name }} == 'schedule' ]]; then
./miri toolchain HEAD --host ${{ matrix.host_target }}
else
./miri toolchain "" --host ${{ matrix.host_target }}
echo "Building against latest rustc git version"
git ls-remote https://github.com/rust-lang/rust/ HEAD | cut -f 1 > rust-version
fi
./miri toolchain --host ${{ matrix.host_target }}
- name: Show Rust version
run: |