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

On 2019-06-17 23:27, Magnus Hagander wrote:
> On Mon, Jun 17, 2019 at 3:03 PM Dave Page <dpage(at)pgadmin(dot)org> wrote:
<snip>
>> Maybe, but there was discussion, and plenty of time for people to
>> object,
>> which noone did.
>
> Well, nobody in that discussion pointed out that we'd have to have a
> message that was that unfriendly :/ Had people known, they might have
> objected...

Looking at the current wording, eg example message from 3 hours ago:

https://github.com/postgres/postgres/pull/41#issuecomment-502660775

The text now seems friendly enough, though it could do with a bit more
white space for readability:

> 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.

Is that feasible?

+ Justin