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

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

>
>
> On Thu, Jul 11, 2019 at 3:10 PM Magnus Hagander <magnus(at)hagander(dot)net>
> wrote:
>
>> 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..)
>>
>
> 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
> :-(
>
>
Ugh. Had I known that I would've strongly objected to installing it in the
first place.

No way to just remove it's permissions on some repos or something? Or it
actually somehow has "organisation superpowers"?

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