Re: GitHub Mirror is broken

2019-03-31 Thread Manuel M T Chakravarty
Thanks! Manuel > Am 31.03.2019 um 17:09 schrieb Ben Gamari : > > Manuel M T Chakravarty writes: > >> I think, it also only mirrors master, but not other branches, which is >> unfortunate especially for release branches. >> > Fixed on both counts. The GitHub mirror should be both up-to-date

Re: GitHub Mirror is broken

2019-03-31 Thread Ben Gamari
Manuel M T Chakravarty writes: > I think, it also only mirrors master, but not other branches, which is > unfortunate especially for release branches. > Fixed on both counts. The GitHub mirror should be both up-to-date and include all branches. Cheers, - Ben signature.asc Description: PGP

Re: GitHub Mirror is broken

2019-03-31 Thread Manuel M T Chakravarty
I think, it also only mirrors master, but not other branches, which is unfortunate especially for release branches. Manuel > Am 31.03.2019 um 05:52 schrieb Phyx : > > Hi Ben, > > I think the mirror is stuck again. Hasn't updated in 8 days. > > Cheers, > Tamar > > On Tue, Feb 19, 2019 at

Re: GitHub Mirror is broken

2019-03-30 Thread Phyx
Hi Ben, I think the mirror is stuck again. Hasn't updated in 8 days. Cheers, Tamar On Tue, Feb 19, 2019 at 6:30 AM Ben Gamari wrote: > Artem Pelenitsyn writes: > > > Hello devs, > > > > This is just to let you know that the latestes commit on GitHub ghc/ghc > > repo dates back to 22th of

Re: GitHub Mirror is broken

2019-02-18 Thread Ben Gamari
Artem Pelenitsyn writes: > Hello devs, > > This is just to let you know that the latestes commit on GitHub ghc/ghc > repo dates back to 22th of January. Personally, I find GitHub mirror quite > useful for ocasional searches over the code base. Therefore, I'd > appreciated repairing the mirror. >