From f2e808034ad1a617e9dbc88ba9223ee49bd85a2a Mon Sep 17 00:00:00 2001 From: lingrui96 <47836765+lingrui96@users.noreply.github.com> Date: Fri, 7 Aug 2026 16:46:30 +0200 Subject: [PATCH] AGENTS.md: add a pushing section The repository has no written rule for how work reaches main, which came up when an agent had to decide between pushing to main directly, the habit visible in the history, and opening a pull request. This states the pull request flow as an instruction rather than a proposal, per the review on #1. Two clauses come from what went wrong on #1 rather than from principle. Force push is allowed only before review, since the branch there was rebuilt to scrub a hostname, which is legitimate while nobody has reviewed and destructive once someone has. And hostnames are kept out of pull request descriptions, not just result files, since the first description of #1 quoted several and had to be edited. Co-Authored-By: Claude Opus 5 --- AGENTS.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/AGENTS.md b/AGENTS.md index cce3b5a..737a088 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -42,6 +42,20 @@ hardware fields in `run.yaml` carry the identity. move all the crates together, and never mix backend features across them. A bump can change measured numbers, so it belongs in its own commit with a rerun. +## Pushing + +Work lands on main through a pull request rather than a direct push. An agent +may push a branch and open the pull request when asked to, and the merge stays +a human decision. Force push only while a branch is still unreviewed: after +someone has reviewed, a force push detaches their comments from the code they +describe. + +A pull request that adds or replaces `result//` states in its +description which machine produced the sweep, so the numbers are reviewed +together with the hardware behind them. Keep hostnames out of the description +as well as out of the files: on a public repository a hostname leaks the +operator's institution and location over time. + ## Prose style No em dashes or en dashes anywhere in this repository's documents, comments or