CI: a branch's pushes run nothing, its pull request runs once
CI / build (pull_request) Successful in 8m43s

A branch with an open pull request ran twice per push: once for the push,
once for the pull request. Pushes to main still run the tests and publish
the badges; every other branch is tested by its pull request.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhqxQ49eCju4CzKYNjZzwT
This commit is contained in:
2026-10-06 16:17:52 +02:00
co-authored by Claude Sonnet 5.5
parent d490a18b9a
commit e2f00e93c2
3 changed files with 7 additions and 6 deletions
+5 -4
View File
@@ -1,7 +1,8 @@
# CI and releases (docs/milestones/R1.md).
# A push: the host tests, with their coverage of lib/. On main, the README's badges
# are published to the branch `badges`.
# A pull request: the same, then the release firmware and the Debug Build.
# A push to main: the host tests, with their coverage of lib/, and the README's badges
# published to the branch `badges`.
# A pull request: the same tests and coverage, then the release firmware and the Debug Build.
# A branch's pushes run nothing by themselves: its pull request runs, once.
# A tag v*: all of it, then a Gitea release with the signed Update File.
# Run by hand: the release of a tag that exists already (the ones from before CI).
#
@@ -11,7 +12,7 @@
name: CI
on:
push:
branches: ['**', '!badges'] # badges holds what CI itself publishes
branches: [main] # other branches are tested by their pull request: one run, not two
tags: ['v*']
pull_request:
workflow_dispatch: