Merge dev: scope-then-rank searches (#4958, #4961), CI gate on integration, milestone 456 steps 4-6 #205

Merged
bvandeusen merged 9 commits from dev into main 2026-10-05 22:23:48 -04:00
Showing only changes of commit 17f4348711 - Show all commits
+7 -1
View File
@@ -328,7 +328,13 @@ jobs:
# wouldn't un-publish a bad hook anyway: the push already did that. A failed
# `plugin` job still turns the whole run red, which is the signal that
# matters.
needs: [typecheck, lint, test]
#
# `integration` IS in needs (rule 177, #4958). It was added after this
# gate and left out of it, so on 2026-10-05 main run 8212 published
# :latest with integration red. The image carries the migrations and the
# queries that lane runs against real Postgres; a red integration run is
# a red image.
needs: [typecheck, lint, test, integration]
# Build on dev, main, and v* tag pushes. dev → :dev, main → :latest,
# tag → :latest + :<version>; every build also gets an immutable :<sha>.
if: github.ref == 'refs/heads/dev' || github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/v')