add a way to run CI on external PRs using a label

This commit is contained in:
Pierre Chapuis 2023-12-14 17:50:22 +01:00
parent 3ff7719cb8
commit c27fd62fc5

View file

@ -1,9 +1,13 @@
name: CI
on: push
on:
push:
pull_request_target:
types: [labeled]
jobs:
lint_and_typecheck:
if: ${{ github.event.name == 'push' || github.event.label.name == 'run-ci' }}
runs-on: ubuntu-latest
steps: