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

On Fri, Jun 28, 2019 at 2:16 PM Magnus Hagander <magnus@hagander.net> wrote:

On Tue, Jun 18, 2019 at 6:18 PM Stephen Frost <sfrost@snowman.net> wrote:

Greetings,

* Magnus Hagander (magnus@hagander.net) wrote:
> On Tue, Jun 18, 2019 at 4:00 PM Stephen Frost <sfrost@snowman.net> wrote:
> > * Justin Clift (justin@postgresql.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. :(
>
> I would say "don't work with" rather than "can't handle".

Sure, that's fine.

> > 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
> > --------------
>
> That does sound a lot better. It should also include pgweb, which also has
> a mirror there.

Ah, yes, agreed.

Is there any actual progress made here?

We're still sending badly formatted replies, and we're still sending replies to pgweb PRs that don't mention what to do about pgweb... 

Ping?

This is still broken AFAICT...