.github: trim number of runners started on push + pr

Signed-off-by: Joachim Wiberg <troglobit@gmail.com>
This commit is contained in:
Joachim Wiberg
2025-07-09 11:50:39 +02:00
parent 5599aca0a3
commit 31b78817dd
2 changed files with 10 additions and 2 deletions
+7 -2
View File
@@ -8,14 +8,19 @@ on:
- '**'
- '!dev'
pull_request:
branches:
- '**'
types: [opened, synchronize, reopened, labeled]
concurrency:
group: ${{ github.workflow }}-${{ github.head_ref || github.ref }}
cancel-in-progress: true
jobs:
build:
# Verify we can build on latest Ubuntu with both gcc and clang
name: ${{ matrix.compiler }}
runs-on: ubuntu-latest
# Skip redundant builds for PRs - prefer PR builds over push builds
if: github.event_name != 'push' || github.ref == 'refs/heads/master'
strategy:
matrix:
compiler: [gcc, clang]
+3
View File
@@ -2,12 +2,15 @@ name: Dotty the Documenteer
on:
push:
branches:
- master
paths:
- 'doc/**'
- 'README.md'
- 'mkdocs.yml'
- '.github/workflows/docs.yml'
pull_request:
types: [opened, synchronize, reopened, labeled]
paths:
- 'doc/**'
- 'README.md'