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

Signed-off-by: Joachim Wiberg <[email protected]>

Author: troglobit

.github/workflows/build.yml

@@ -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]

.github/workflows/docs.yml

@@ -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'