summaryrefslogtreecommitdiff
path: root/.github/workflows
diff options
context:
space:
mode:
authorEnguerrand Decorne <decorne.en@gmail.com>2021-10-07 10:06:37 +0200
committerEnguerrand Decorne <decorne.en@gmail.com>2021-10-07 10:29:53 +0200
commite032c53944dd01a89ce2c885717d0c902a3882ac (patch)
treee159281af8ea2bbf5809ea6d6d2e11bcb0cf6c36 /.github/workflows
parent4db86d2d3eeaf45f38d8fb4968b1fe43d9ba5bd2 (diff)
downloadocaml-e032c53944dd01a89ce2c885717d0c902a3882ac.tar.gz
disable changes check on 5.0
Diffstat (limited to '.github/workflows')
-rw-r--r--.github/workflows/hygiene.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/workflows/hygiene.yml b/.github/workflows/hygiene.yml
index e76ba6b949..e0707edcc5 100644
--- a/.github/workflows/hygiene.yml
+++ b/.github/workflows/hygiene.yml
@@ -33,6 +33,7 @@ jobs:
if: >-
!contains(github.event.pull_request.labels.*.name, 'no-change-entry-needed')
&& github.event_name == 'pull_request'
+ && github.event.pull_request.base.ref != '5.00'
- name: configure correctly generated
run: >-