CI breakage from #13556

Stream: mathlib4

[Joseph Myers]

I think #13556 (ci: report changes to the import graph in a spoiler comment) has broken CI for any PR based on a mathlib version including that PR. I'm seeing error: pathspec 'origin/import-count' did not match any file(s) known to git in an unrelated new PR (#13580).

[Andrew Yang]

Try again. Should work now. We definitely need the "follow up PR" mentioned in #13556

[Andrew Yang]

I pushed re-run and it indeed works.

[Bryan Gin-ge Chen]

Ah, thanks. I could have sworn I checked that the branch name used in the script was different from the one used for the PR but I must have been looking at a different page...

edit: as penance I've created #13581