Merge #4844

4844: tullia jobs: use generic gitrev for PRs r=jbgi a=jbgi to avoid unnecessary builds of big artifact, like dockerImages. Goal: bors ci build should not build anything if branch is up-to-date and ci pass. Some other minor clean-ups. Co-authored-by: Jean-Baptiste Giraudeau <jb@giraudeau.info>
IntersectMBO · Jan 26, 2023 · 0747007 · 0747007
2 parents 9675f4b + 0ceeeec
commit 0747007
Show file tree

Hide file tree

Showing 6 changed files with 246 additions and 245 deletions.
diff --git a/bors.toml b/bors.toml
@@ -1,5 +1,5 @@
 status = [
-  "ci/push/required",
+  "ci/pr/required",
 ]
 timeout_sec = 7200
 required_approvals = 1

diff --git a/flake.lock b/flake.lock