[postgis-devel] GH Issues Migration Report Out

[Regina Obe]

>> So what else can I possibly gain from having tickets on github or even having github as official repo.  So it's easier for you to click the Merge button?

> This is still an interesting question.
> And I'm hoping that the new "github team" lead by Kompza will smooth out more things (I do can think of ways to make the green button clickably, only have no interest to learn how to use proprietary platforms, but if others do... please > focus on these things!)

> --strk;

One thought I had which would be cool and I'd be willing to entertain is to have a special label.  It's almost as good as a merge button and all our mirrors support labels.
We use the label feature of github/gitea/gitlab -- define a label that a bot I will refer to as 

Pullie

Will monitor.

This will work for all our mirrors.

When the label is added to the pull request, Pullie will then consider it a merge request, commit to our repo if it passes all her tests,
And then closes the pull request and (ideally the associated ticket if any. Though that may be trickier).