managing a long list of comments on github

Stream: mathlib4

[Antoine Chambert-Loir]

PR #6057 has more than 250 commits/comments etc. and when I open the page, those I'm interested in are hidden, I need to click an indefinite number of times to have them appear.
Is there a more convenient way to do that?

[Ruben Van de Velde]

I'm not aware of one

[Alex J. Best]

Maybe the refined github extension will help you https://github.com/refined-github/refined-github?tab=readme-ov-file#reading-comments.