Skip to content

Runner: --include-prs records the PRs since the previous result set - #78

Merged
NullVoxPopuli merged 1 commit into
NullVoxPopuli:mainfrom
NullVoxPopuli-ai-agent:include-prs-in-notes
Jul 29, 2026
Merged

Runner: --include-prs records the PRs since the previous result set#78
NullVoxPopuli merged 1 commit into
NullVoxPopuli:mainfrom
NullVoxPopuli-ai-agent:include-prs-in-notes

Conversation

@NullVoxPopuli-ai-agent

Copy link
Copy Markdown
Contributor

The latest result set's notes.prs was collected by hand (6086a0c). This adds --include-prs so the runner records it instead — from git history alone, no GitHub API.

How it works

  • "When was the last result set?" Result files are named with the run's ISO timestamp, so the previous set's date is simply the newest filename in results/public/results/ other than the file being written — which also does the right thing when appending to today's file (the previous set becomes the one before it).

  • "Which PRs landed since?" git log --since=<that date>, matching both merge shapes:

    • merge commits: Merge pull request #N from ... in the subject, PR title as the first body line
    • squash merges: The PR title (#N) in the subject

    Deduplicated by number, newest first.

  • The list is printed before the "does this information look correct?" confirm, so what will be recorded is part of the pre-run review.

  • Saved as notes.prs entries of { url, title }, merged with whatever is already there and deduplicated by URL — hand-added entries (plain URL strings, like the existing file) and earlier appends survive.

Results app

The run-info block (<Info />) now shows the list in a <details>:

PRs since the previous result set (3)

Runner-recorded entries render as #76 — <title>; hand-added string entries render as just #72 (both link to the PR). The existing 2026-07-29 result set's hand-added notes render as-is, verified in the dev server at 1920px along with the titled shape.

Verified

🤖 Generated with Claude Code

The latest result set's notes.prs was hand-collected. With
--include-prs the runner records it instead: result files are named
with the run's ISO timestamp, so the previous result set's date is the
newest other filename, and the PRs that landed since come from git
history alone (no GitHub API) -- merge commits carry the number in the
subject and the title in the body, squash merges carry both in the
subject.

The list is printed before the 'does this look correct?' confirm, and
merged into notes.prs deduplicated by URL, so hand-added entries (plain
URL strings) and earlier appends survive.

The results app shows the list in a <details> under the run info:
'NullVoxPopuli#76 <title>' for runner entries, 'NullVoxPopuli#72' for hand-added strings.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@vercel

vercel Bot commented Jul 29, 2026

Copy link
Copy Markdown

@NullVoxPopuli-ai-agent is attempting to deploy a commit to the NullVoxPopuli's projects Team on Vercel.

A member of the Team first needs to authorize it.

@vercel

vercel Bot commented Jul 29, 2026

Copy link
Copy Markdown

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated (UTC)
rere-benchmark Ready Ready Preview, Comment Jul 29, 2026 3:01pm

@NullVoxPopuli
NullVoxPopuli merged commit aabd19e into NullVoxPopuli:main Jul 29, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants