diff options
| author | Francois Kritzinger <francois@codesynthesis.com> | 2024-12-12 14:22:18 +0200 |
|---|---|---|
| committer | Francois Kritzinger <francois@codesynthesis.com> | 2024-12-13 11:09:58 +0200 |
| commit | 4108a65af34829c5dd7e350ca1058eb4e0e4eee4 (patch) | |
| tree | cc8e84e64951172a168f3633361e601bb256dc8d /INSTALL-GITHUB-DEV | |
| parent | d50e2ae861180d6f965b0c4dee4d401d01f571b5 (diff) | |
ci-github: Cancel CI when history is overwritten
Cancel CI for previous, now-overwritten head commit when a forced push is
done.
Diffstat (limited to 'INSTALL-GITHUB-DEV')
| -rw-r--r-- | INSTALL-GITHUB-DEV | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/INSTALL-GITHUB-DEV b/INSTALL-GITHUB-DEV index 244d26c..716ed28 100644 --- a/INSTALL-GITHUB-DEV +++ b/INSTALL-GITHUB-DEV @@ -63,9 +63,11 @@ At this stage the only settings we need to update are: - Checks: RW - Metadata (mandatory): RO - Pull requests: RO + - Contents: RO (for Push events) - Subscribed events - Check suite - Pull request + - Push Click "Create GitHub App" button. When the page reloads: |