ci: Trigger CI also on PRs to develop/* branches

[paulgessinger]

This is needed for backporting.

[codecov]

Codecov Report

Merging #1367 (f9b5e2c) into main (789ce69) will not change coverage.
The diff coverage is n/a.

❗ Current head f9b5e2c differs from pull request most recent head efae8e4. Consider uploading reports for the commit efae8e4 to get more accurate results

@@           Coverage Diff           @@
##             main    #1367   +/-   ##
=======================================
  Coverage   47.83%   47.83%           
=======================================
  Files         380      380           
  Lines       20149    20149           
  Branches     9371     9371           
=======================================
  Hits         9638     9638           
  Misses       4063     4063           
  Partials     6448     6448           

📣 Codecov can now indicate which changes are the most critical in Pull Requests. Learn more

[acts-project-service]

The backport to develop/v19.x failed:

The process '/usr/bin/git' failed with exit code 1

To backport manually, run these commands in your terminal:

# Fetch latest updates from GitHub
git fetch
# Create a new working tree
git worktree add .worktrees/backport-develop/v19.x develop/v19.x
# Navigate to the new working tree
cd .worktrees/backport-develop/v19.x
# Create a new branch
git switch --create backport-1367-to-develop/v19.x
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 f956eb3e3f54362126fbd31572541f391a0f06ef
# Push it to GitHub
git push --set-upstream origin backport-1367-to-develop/v19.x
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-develop/v19.x

Then, create a pull request where the base branch is develop/v19.x and the compare/head branch is backport-1367-to-develop/v19.x.