From 765655106c1a8f67ebbcdc9d9abf9713f7187fbe Mon Sep 17 00:00:00 2001
From: thc1006 <84045975+thc1006@users.noreply.github.com>
Date: Sat, 8 Aug 2026 11:03:41 +0800
Subject: [PATCH] CI: build the docs for pull requests into develop as well

`branches` filters on a pull request's base, and almost every PR here is opened
against develop: 25 of the last 30, with 3 against master. So the build that
runs with -W --keep-going saw a docs change for the first time in a release
batch, well away from whatever caused it.

The path filter already keeps this off PRs that cannot affect the docs, and
`rocketpy/**` is in it because docstrings feed the autodoc reference, so a
docstring edit merged into develop could break the API pages unnoticed too.

`push` is left on master alone. The pull request check is where the feedback is
worth having, and running both would double the cost for a second opinion on
the same commit.

Signed-off-by: thc1006 <84045975+thc1006@users.noreply.github.com>
---
 .github/workflows/docs.yml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 806bef0dc..3d7657b84 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -1,10 +1,12 @@
 name: Documentation
 
 on:
-  # Only PRs targeting master (base branch = master) and pushes to master.
+  # PRs into either long-lived branch, and pushes to master. `branches` filters
+  # on the PR's base, and almost every PR is opened against develop, so master
+  # alone meant the build first saw a docs change in the release batch.
   pull_request:
     types: [opened, synchronize, reopened, ready_for_review]
-    branches: [master]
+    branches: [master, develop]
     paths:
       - "docs/**"
       - "rocketpy/**" # docstrings feed the autodoc API reference