diff options
| -rw-r--r-- | src/tools/miri/.github/workflows/ci.yml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/tools/miri/.github/workflows/ci.yml b/src/tools/miri/.github/workflows/ci.yml index 7d8c7203b32..8b0916f5111 100644 --- a/src/tools/miri/.github/workflows/ci.yml +++ b/src/tools/miri/.github/workflows/ci.yml @@ -12,12 +12,6 @@ on: schedule: - cron: '44 4 * * *' # At 4:44 UTC every day. -permissions: - # The cronjob needs to be able to push to the repo... - contents: write - # ... and create a PR. - pull-requests: write - defaults: run: shell: bash @@ -93,6 +87,11 @@ jobs: cron-fail-notify: name: cronjob failure notification runs-on: ubuntu-latest + permissions: + # The cronjob needs to be able to push to the repo... + contents: write + # ... and create a PR. + pull-requests: write needs: [build, style] if: github.event_name == 'schedule' && failure() steps: |