github? [Re: [Agda] Agda development]

[Jan Stolarek]

> 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