On 12/09/18 10:54, Chris McCormick wrote:
On 11/09/18 20:55, IOhannes m zmoelnig wrote:
personally, i always do a local investigation of PRs before merging them
For those who find the presence of GitHub's green "merge" button to be a
deeply offensive abomination[1], there is this userscript (which you can
install with Tampermonkey or similar) for hiding it automatically:
Here is the correct link:
https://gist.github.com/aripollak/4322621/
Cheers,
Chris.
--
http://mccormick.cx/
_______________________________________________
Pd-dev mailing list
[email protected]
https://lists.puredata.info/listinfo/pd-dev