PSA: broken diff selection on github

Stream: mathlib4

[Eric Wieser]

The usual "look at the diff between commits[3] and commits[-1] approach" to ported files is still possible on github, but the UI for it is broken. If you try and shift click in the commit view, it generates a broken URL with 8-character SHAs.

Thankfully it still works if you replace those short SHAs with the full 40-character SHAs.

[Eric Wieser]

Hmm, it seems I might have just hit a (short) SHA collision which Github handles incorrectly

[Eric Wieser]

Can anyone else reproduce on !4#3716?