Two corrections from Kaj, both mine.
istvan is pisti87. I had been thanking them as two people across beta_64 and the
beta_65 stable notes, which splits one person's contribution in half and reads as
if a second reporter existed. Merged into pisti87 everywhere: both notes files,
the source comment that cited the report, both published GitHub bodies, and the
on-device stable notes, which are generated from the cumulative notes file and
had to be regenerated and redeployed.
And in beta_67 I turned Discord names into GitHub @-mentions. "@Jade" resolves to
an unrelated GitHub account, so a stranger got tagged on our release, and the
handle credited was not the person who did the work. The names stay, as plain
text, and the @ is gone.
The rule I should have been following: an @-mention is only safe when the handle
came from GitHub itself, i.e. the author of a PR, issue or commit. @cvhviz,
@pisti87, @oumike, @wb6zsu, @Yoss101 all came from GitHub and are fine. A name
seen in chat is a display name, not a handle, and mapping one to the other is a
guess that lands on somebody real.
Not rewritten: commit messages already pushed that mention istvan. History stays
as it is; the user-facing credits are what matter and those are corrected.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
