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