GitHub pull requests

Alexander Berntsen alexander at plaimi.net
Tue Oct 21 08:36:29 UTC 2014


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

On 21/10/14 09:18, Alexander Berntsen wrote:
> On 20/10/14 21:13, Ben Gamari wrote:
>> > 
>> >  1. Do nothing, ignore pull requests as we do now
>> > 
>> >  2. Monitor Github for new pull requests and close with a message
>> >     requesting that the user opens a differential instead
> This is stupid. Instead, disable pull requests on GitHub altogether.
Apparently PRs are no longer a feature which may be disabled. (Thanks Merijn, for pointing that out to me.) So I guess I vote for 1 bar anyone taking the time to do 3 and optionally also 4.
- -- 
Alexander
alexander at plaimi.net
https://secure.plaimi.net/~alexander
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iF4EAREIAAYFAlRGGw0ACgkQRtClrXBQc7UQ7AD+IFkEomzkhbXIQKynvYgcrTzI
OamTaaXKeBBT54rG2cIBAIl2fESCyTGTbeYETRV58QiNAuGZ/4Tf+hfohfiHFDPE
=ydbf
-----END PGP SIGNATURE-----


More information about the ghc-devs mailing list