Re: A small documentation PR on github

Alexander Kjeldaas writes:

Hi devs!

I created a small documentation PR for the GHC FFI on github and noticed that there's another one-liner PR from May 2019 that was not merged.

https://github.com/ghc/ghc/pull/260 https://github.com/ghc/ghc/pull/255

Just checking that simple PRs are still accepted on github.

An excellent point. In my mind the move to GitLab has addressed the principle reason why we started accepted small PRs on GitHub. My sense is that we should move these PRs to GitLab and formally stop accepting PRs via GitHub. If there is no objection I will do this in three days. Cheers, - Ben