<div dir="ltr"><div dir="ltr">Wrt my change, I've made a merge request on Gitlab.  Absolutely no problems using that tool.</div><div><br></div><div>Alexander<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jul 4, 2020 at 2:28 AM Moritz Angermann <<a href="mailto:moritz.angermann@gmail.com">moritz.angermann@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div dir="auto">The performance of GH is still better than GL. Reading the code on GH is faster and easier to navigate than GL. This might be an artifact of my location? The GL UI feels a lot more sluggish. Though GH is doing their part with service downtimes recently as well. </div></div><div dir="auto"><br></div><div dir="auto">Making a small change on GH to a file is almost comically trivial. Press Edit, make the change, commit and open the PR. All from within the browser in a few seconds. Wasn’t this this primary motivation for allowing documentation PRs on GH?</div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 4 Jul 2020 at 2:18 AM, Ben Gamari <<a href="mailto:ben@smart-cactus.org" target="_blank">ben@smart-cactus.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Alexander Kjeldaas <<a href="mailto:alexander.kjeldaas@gmail.com" target="_blank">alexander.kjeldaas@gmail.com</a>> writes:<br>
<br>
> Hi devs!<br>
><br>
> I created a small documentation PR for the GHC FFI on github and noticed<br>
> that there's another one-liner PR from May 2019 that was not merged.<br>
><br>
> <a href="https://github.com/ghc/ghc/pull/260" rel="noreferrer" target="_blank">https://github.com/ghc/ghc/pull/260</a><br>
> <a href="https://github.com/ghc/ghc/pull/255" rel="noreferrer" target="_blank">https://github.com/ghc/ghc/pull/255</a><br>
><br>
> Just checking that simple PRs are still accepted on github.<br>
><br>
An excellent point. In my mind the move to GitLab has addressed the<br>
principle reason why we started accepted small PRs on GitHub. My sense<br>
is that we should move these PRs to GitLab and formally stop accepting<br>
PRs via GitHub.<br>
<br>
If there is no objection I will do this in three days.<br>
<br>
Cheers,<br>
<br>
- Ben<br>
<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div>
</blockquote></div></div>