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

On Thu, Jul 11, 2019 at 1:38 PM Dave Page <dpage(at)pgadmin(dot)org> wrote:

>
>
> On Thu, Jul 11, 2019 at 12:23 PM Magnus Hagander <magnus(at)hagander(dot)net>
> wrote:
>
>>
>>
>> On Thu, Jul 11, 2019 at 12:05 PM Dave Page <dpage(at)pgadmin(dot)org> wrote:
>>
>>>
>>>
>>> On Thu, Jul 11, 2019 at 10:24 AM Magnus Hagander <magnus(at)hagander(dot)net>
>>> wrote:
>>>
>>>> On Fri, Jun 28, 2019 at 2:16 PM Magnus Hagander <magnus(at)hagander(dot)net>
>>>> wrote:
>>>>
>>>>> On Tue, Jun 18, 2019 at 6:18 PM Stephen Frost <sfrost(at)snowman(dot)net>
>>>>> wrote:
>>>>>
>>>>>> Greetings,
>>>>>>
>>>>>> * Magnus Hagander (magnus(at)hagander(dot)net) wrote:
>>>>>> > On Tue, Jun 18, 2019 at 4:00 PM Stephen Frost <sfrost(at)snowman(dot)net>
>>>>>> wrote:
>>>>>> > > * 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. :(
>>>>>> >
>>>>>> > 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..)

--
Magnus Hagander
Me: https://www.hagander.net/ <http://www.hagander.net/>
Work: https://www.redpill-linpro.com/ <http://www.redpill-linpro.com/>