From 4108a65af34829c5dd7e350ca1058eb4e0e4eee4 Mon Sep 17 00:00:00 2001
From: Francois Kritzinger <francois@codesynthesis.com>
Date: Thu, 12 Dec 2024 14:22:18 +0200
Subject: ci-github: Cancel CI when history is overwritten

Cancel CI for previous, now-overwritten head commit when a forced push is
done.
---
 INSTALL-GITHUB-DEV | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'INSTALL-GITHUB-DEV')

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:
 
-- 
cgit v1.1