12 Sep
2018
12 Sep
'18
9:33 a.m.
On 2018-09-12 04: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:
rofl.
gasmdr IOhannes