GitLab Migration (CI heads-up)
ben at smart-cactus.org
Sat Dec 22 15:26:34 UTC 2018
Gabor Greif <ggreif at gmail.com> writes:
> (following-up own mail)
> This seems resolved too. I have submitted my branch into the main
> repo, and now the pipeline is executing :-)
> Still, do we want running pipelines for external contributors too?
Indeed we do. Small oversight on my part; now fixed.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 487 bytes
Desc: not available
More information about the ghc-devs