mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Auto merge of #2948 - RalfJung:cron, r=RalfJung

Browse Source 
cronjob auto-PR: make sure we are on a branch

Also run this every hour to speed up testing
This commit is contained in:
bors 2023-07-02 09:47:25 +00:00
commit 9e49f537c8
2 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -11,6 +11,7 @@ on:
- 'master' - 'master'
schedule: schedule:
- cron: '6 6 * * *' # At 6:06 UTC every day. - cron: '6 6 * * *' # At 6:06 UTC every day.
- cron: '42 * * * *' # Also each hour, for testing
env: env:
CARGO_UNSTABLE_SPARSE_REGISTRY: 'true' CARGO_UNSTABLE_SPARSE_REGISTRY: 'true'
@ -196,7 +197,10 @@ jobs:
git config --global user.name 'The Miri Conjob Bot' git config --global user.name 'The Miri Conjob Bot'
git config --global user.email 'miri@cron.bot' git config --global user.email 'miri@cron.bot'
- name: get changes from rustc - name: get changes from rustc
run: ./miri rustc-pull run: |
git status # just to see more of what is happening
git checkout master # by default we are not on a branch
./miri rustc-pull
- name: Install rustup-toolchain-install-master - name: Install rustup-toolchain-install-master
run: cargo install -f rustup-toolchain-install-master run: cargo install -f rustup-toolchain-install-master
- name: format changes (if any) - name: format changes (if any)

2
src/tools/miri/miri
View File

@ -124,7 +124,7 @@ rustc-pull)
git commit rust-version -m "Preparing for merge from rustc" || (echo "FAILED to commit rust-version file, something went wrong"; exit 1) git commit rust-version -m "Preparing for merge from rustc" || (echo "FAILED to commit rust-version file, something went wrong"; exit 1)
# Fetch given rustc commit and note down which one that was # Fetch given rustc commit and note down which one that was
git fetch http://localhost:8000/rust-lang/rust.git@$FETCH_COMMIT$JOSH_FILTER.git || (echo "FAILED to fetch new commits, something went wrong"; exit 1) git fetch http://localhost:8000/rust-lang/rust.git@$FETCH_COMMIT$JOSH_FILTER.git || (echo "FAILED to fetch new commits, something went wrong"; exit 1)
git merge FETCH_HEAD --no-ff -m "Merge from rustc" || (echo "FAILED to merge new commits, something went wrong"; exit 1) git merge FETCH_HEAD --no-ff -m "Merge from rustc" || (echo "FAILED to merge new commits ($(git rev-parse FETCH_HEAD)), something went wrong"; exit 1)
exit 0 exit 0
;; ;;
rustc-push) rustc-push)