SIGN IN SIGN UP

Refresh pull requests after a manual fetch

The background fetch path already includes PULL_REQUESTS in its
post-fetch refresh scope, but the manual fetch from the files view
doesn't. As far as I can tell that's an oversight from when
PULL_REQUESTS was added — there's no reason the two paths should
differ. Align them so both refresh PRs after fetching.

This also sets up the next commit to extract a shared helper for
the post-fetch refresh.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
S
Stefan Haller committed
77652863c4c152fce1d2556db15c5ce3b9702bdf
Parent: 7d1d90a