Re: GitHub pull requests

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

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.

>  3. Teach Phabricator to allow to submit a URL to a commit (or branch)
>     in a forked github.com/ghc/ghc repo, and create a code-revision out
>     of that. (suggested by hvr)
>     
>  4. Monitor Github for new pull requests and use facility in (3) to 
>     open a differrential and close the pull request with a message
>     pointing to it.
If someone can be bothered implementing these, they could work.

>  5. Start accepting pull requests in addition to differentials
>     (suggested by Joachim)
- -1.
- -- 
Alexander
alexander@plaimi.net
https://secure.plaimi.net/~alexander
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iF4EAREIAAYFAlRGCKsACgkQRtClrXBQc7U5jgD+NFGH9wNB8t54K8v2xjOQ3U1a
T4W6hPkKbmUNrdPjf2YA/0eDUG2XJgEvxiuSnVtmimLgrGFc2weD9f1656/S2tm8
=3ELn
-----END PGP SIGNATURE-----