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: Feb 05 2023 at 22:03 UTC