I could (and in fact the script names the remote directly already,
because you can't pass refspecs without specifying the remote). But I do
occasionally push a single branch with a bare "git push". Usually this
is the integration branch, when I am trying to trigger CI manually
(e.g., when piling hacks on top in order to debug a CI failure ;) ).

So even if I only do it infrequently, it feels weird that a bare "git
push" would try to push to the upstream remote (which I don't even have
write access to!).

Maybe ’push.default=simple’ or ’push.default=nothing’ are better settings
in your scenario. Then you get explicit pushing because no push branch gets
set. And thus 'git status' reports not additinal status.

Yeah, though @{push} is usually not explicitly configured in the same
way @{upstream} is, but rather a consequence of how push.default and
remote.pushdefault interact. But it was added for exactly this kind of
triangular workflow. I sometimes will do stuff like:

  git range-diff origin @{push} HEAD

I imagine the same thing could be achieved with

    origin/$(git rev-parse --abbrev-ref HEAD)


Harald