Sure, we can try with actions first. It does not change the implementation
of the bot much, just makes persisting the bot's state a bit more
complicated. (But that problem has been solved before by others.)
On Tuesday, February 7, 2023 at 11:00:14 PM UTC+2 Matthias Koeppe wrote:
> I think curr
I think currently the only time when there is a shortage of GH Actions
runners is after pushing a release tag because then we run the full
portability suite, which spins up dozens of builds.
On Tuesday, February 7, 2023 at 12:58:04 PM UTC-8 Dima Pasechnik wrote:
>
>
> On Tue, 7 Feb 2023, 20:55
On Tue, 7 Feb 2023, 20:55 Matthias Koeppe, wrote:
> On Tuesday, February 7, 2023 at 5:33:04 AM UTC-8 David Roe wrote:
> On Tue, Feb 7, 2023 at 10:28 AM Eric Gourgoulhon
> wrote:
> * Julian and I can work on creating a bot for managing component teams.
> There will be a top level "Components" tea
On Tuesday, February 7, 2023 at 5:33:04 AM UTC-8 David Roe wrote:
On Tue, Feb 7, 2023 at 10:28 AM Eric Gourgoulhon
wrote:
* Julian and I can work on creating a bot for managing component teams.
There will be a top level "Components" team, with a sub-team associated to
each of our existing comp
On Tue, 7 Feb 2023 at 16:49, David Roe wrote:
> In response to Eric's suggestion of having the whole team set as the
> reviewer, my main concern is that having a diffuse responsibility will make
> it more likely for tickets to slip through the cracks. If you want to
> review a ticket and someone
In response to Eric's suggestion of having the whole team set as the
reviewer, my main concern is that having a diffuse responsibility will make
it more likely for tickets to slip through the cracks. If you want to
review a ticket and someone else is assigned by the bot, I think taking
over as revi
On Tue, 7 Feb 2023, 16:39 John Cremona, wrote:
> Re David's #1: Could we only allow PRs to be made by members? (Or is
> that against the spirit of open source?) Then, a new contributor would
> first ask to become a member, and then would be able to make a PR.
>
on trac, everyone with a GitHu
Re David's #1: Could we only allow PRs to be made by members? (Or is
that against the spirit of open source?) Then, a new contributor would
first ask to become a member, and then would be able to make a PR.
John
On Tue, 7 Feb 2023 at 16:29, Eric Gourgoulhon
wrote:
> Thanks for your reply.
>
Thanks for your reply.
Le mardi 7 février 2023 à 14:33:04 UTC+1, David Roe a écrit :
4. When a component tag is added to a PR (or a new PR created with a
component set), if there is no reviewer already requested then the bot will
request review from someone on that component team (eventually
On Tue, 7 Feb 2023, 13:33 David Roe, wrote:
>
>
> On Tue, Feb 7, 2023 at 10:28 AM Eric Gourgoulhon
> wrote:
>
>> Hi,
>>
>> Thanks again for all the hard work for the github migration!
>>
>> I would like to create a team "Manifolds" of https://github.com/sagemath,
>> with sufficient permissions s
On Tue, Feb 7, 2023 at 10:28 AM Eric Gourgoulhon
wrote:
> Hi,
>
> Thanks again for all the hard work for the github migration!
>
> I would like to create a team "Manifolds" of https://github.com/sagemath,
> with sufficient permissions so that I can add users to it. How shall I
> proceed? Are ther
Hi,
Thanks again for all the hard work for the github migration!
I would like to create a team "Manifolds" of https://github.com/sagemath,
with sufficient permissions so that I can add users to it. How shall I
proceed? Are there any team creation request on the github interface or
should some
12 matches
Mail list logo
