Stream: Coq devs & plugin devs

Topic: refined github


view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:20):

I've been using https://github.com/refined-github/refined-github recently and I have had a pleasent experience. It has various quality of life improvements to the standard GitHub UI. Thought others here might be interested too.

view this post on Zulip Ali Caglayan (Jan 26 2022 at 13:25):

@Gaëtan Gilbert Something you might like, with refined github you can Ctrl click on expand in a github thread and it will expand the whole thing.

view this post on Zulip Ali Caglayan (Feb 16 2022 at 18:16):

Another thing I discovered today, you can hide all collapsed comments and github events, making those spaghetti threads much easier to navigate.


Last updated: Mar 29 2024 at 05:40 UTC