CI improvements (#1012)

This commit is contained in:
Jorge Martin Espinosa
2023-07-31 21:05:28 +02:00
committed by GitHub
parent 8fd71b4126
commit 89b1bba96e
7 changed files with 70 additions and 6 deletions

View File

@@ -5,6 +5,7 @@ on: [pull_request, merge_group]
jobs:
build:
runs-on: ubuntu-latest
# Don't run in the merge queue again if the branch is up to date with `develop`
if: github.event.merge_group.base_ref != 'refs/heads/develop'
name: Validate
steps: