[PD-dev] Thoughts on git & github workflows

[Chris McCormick]

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:

https://news.ycombinator.com/item?id=3960876

Cheers,

Chris.

[1] https://github.com/torvalds/linux/pull/17#issuecomment-5654674

-- 
http://mccormick.cx/