github? [Re: [Agda] Agda development]

[Mateusz Kowalczyk]

On 09/01/14 08:55, Jan Stolarek wrote:
> Good to hear that.
> 
>> We were a bit underwhelmed by the issue tracker on github
> Yes, github's issue tracker has some limitations. Most notable one is no support for attachments.
> 
> An alternative approach you might wish to consider is having git repository on one of your servers 
> and mirroring that repo through github. This is approach used by GHC. I'm not sure whether this 
> is available for free, but someone in the GHC dev team should know (I think).
> 
> Janek
> 

It is free but you have to manually apply for it with GitHub staff. I
believe you have to open a support ticket and ask for it.

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.


-- 
Mateusz K.