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

On Thu, Jul 11, 2019 at 3:10 PM Magnus Hagander <magnus@hagander.net> wrote:

On Thu, Jul 11, 2019 at 1:38 PM Dave Page <dpage@pgadmin.org> wrote:

On Thu, Jul 11, 2019 at 12:23 PM Magnus Hagander <magnus@hagander.net> wrote:

On Thu, Jul 11, 2019 at 12:05 PM Dave Page <dpage@pgadmin.org> wrote:

On Thu, Jul 11, 2019 at 10:24 AM Magnus Hagander <magnus@hagander.net> wrote:

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

As far as I'm aware there's nothing actually broken there at the moment - it just needs an improved message for which I suggested Stephen send a patch.

 

It closes PRs for pgweb referencing postgresql and pgadmin, I consider that broken.

And yes, the message itself needs to be fixed as well. 

What do you mean "as well"? It's supposed to close PRs on all repos. The entire problem is the message as far as I can tell.

 

I mean "as well" only in that it's not part of the suggested text above (which has not been implemented). I *am* just talking about the message, yes.

(Though I assume it is possible to turn it off for individual repos -- there have been discussions about for exampe moving pgweb to actually *use* github for a while as a POC for how things would or wouldn't work for our community, and it wouldn't be good if we've actually prevented any such things for the future..)

As I noted, the only way to do that is to have the config file be in each individual repo on which you want the bot to run, rather than globally. That would mean committing the .github directory to the main source tree :-(