github? [Re: [Agda] Agda development]

[Mateusz Kowalczyk]

On 09/01/14 10:34, Jan Stolarek wrote:
>> I think that using it just as a mirror is rather pointless because you
>> still have to do everything against the main repository (patches &c) as
>> opposed to forming pull requests on GitHub.
> Yes, you are right about that. The question is whether Agda devs intend to use pull requests. They 
> are convenient to use but create lots of empty merge commits which is a good reason to avoid 
> them.
> 
> Janek
> 
You can merge pull requests without using the merge button on GitHub
which avoids the message[1].

Personally I think the message is nice, it shows the path of the commit
history but to each their own.


[1]: https://help.github.com/articles/merging-a-pull-request
-- 
Mateusz K.