Re: Install github app to automatically close PRs on github mirror

Greetings,

* Justin Clift (justin(at)postgresql(dot)org) wrote:
> On 2019-06-17 23:27, Magnus Hagander wrote:
> >Thanks for your Pull Request! :) This repo on GitHub is just a
> >mirror of our real git repositories though, and can't really handle
> >PRs. :( Hopefully you can redo the PR, and direct it to the
> >git.postgresql.org repos? We have a developer guide, if that
> >helps: https://wiki.postgresql.org/wiki/So,_you_want_to_be_a_developer%3F.
> >If this was a PR for pgAdmin, please visit
> >https://www.pgadmin.org/docs/pgadmin4/dev/submitting_patches.html.
>
> Hmmm... that wall of text really could do with breaking up if possible.

Agreed.

What about:

--------------
Thanks for your Pull Request! :) This repo on GitHub is just a
mirror of our real git repository (which lives on git.postgresql.org)
though, and can't really handle PRs. :(

If you'd like to see this change in PostgreSQL, please check out our
developer guide, here:

https://wiki.postgresql.org/wiki/So,_you_want_to_be_a_developer%3F

If this was a PR for pgAdmin, please see this guide instead:

https://www.pgadmin.org/docs/pgadmin4/dev/submitting_patches.html
--------------

Telling people to direct their PR to the git.postgresql.org repos
doesn't really make sense...

Thanks!

Stephen