Skip to content

Stable merge window for week 37 of 2023 #2447

Stable merge window for week 37 of 2023

Stable merge window for week 37 of 2023 #2447

Workflow file for this run

name: pr-labels
on:
pull_request:
types: [opened, reopened, synchronize, edited, labeled, unlabeled]
jobs:
check-labels:
name: Check that PRs against the stable branch are labelled correctly
runs-on: ubuntu-20.04
steps:
- name: Check labels
run: |
[[ '${{ github.base_ref }}' != stable ]] \
|| [[ '${{ contains(github.event.pull_request.labels.*.name, 'merge') }}' == true ]]