From 1640386dd2f7ba449225ffb80ce713211e5a27ef Mon Sep 17 00:00:00 2001
From: Matthias Frei <matzf@scion.org>
Date: Mon, 15 Jul 2024 13:31:43 +0200
Subject: [PATCH] github: add check for PR title

---
 .github/workflows/pr-title.yml | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 .github/workflows/pr-title.yml

diff --git a/.github/workflows/pr-title.yml b/.github/workflows/pr-title.yml
new file mode 100644
index 0000000000..41a54c144c
--- /dev/null
+++ b/.github/workflows/pr-title.yml
@@ -0,0 +1,31 @@
+name: Check the pull request title
+
+on:
+  pull_request:
+    types: [opened, edited, reopened, synchronize]
+
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    steps:
+    - name : Check the PR title
+      env:
+        TITLE: ${{ github.event.pull_request.title }}
+      run: |
+        # Check that PR is of the form `<subsystem>: <lowercase message>`
+
+        url='https://docs.scion.org/en/latest/dev/git.html#good-commit-messages'
+        if [[ ! "$TITLE" =~ ^[a-z0-9,/]*:[[:space:]] ]]; then
+          echo '::error::The PR title should start with `<substystem>: `. See '"$url"
+          exit 1
+        fi
+        # Title should be lower case; initialisms and identifiers still occur occasionally and should be allowed.
+        # -> enforce only the first word
+        if [[ ! "$TITLE" =~ ^[a-z0-9,/]*:[[:space:]][a-z] ]]; then
+          echo '::error::The PR title should be lower case (enforced on first letter). See '"$url"
+          exit 1
+        fi
+        if [[ $TITLE =~ \.[[:space:]]*$ ]]; then
+          echo '::error::The PR title should not end with a ".". See '"$url"
+          exit 1
+        fi