patchbots off

[Frédéric Chapoton]

Hello,

following the recent major changes to our workflow, I will soon turn off the "patchbot server" machine. This will have the side effect of breaking the round "patchbot report" icons in the frozen trac website.

To people running "patchbot clients", please stop your machines. You may want to turn them to runners in our new setting, but please do not ask me how.

Frédéric

[Dima Pasechnik]

On Mon, Feb 13, 2023 at 1:29 PM Frédéric Chapoton <fchap...@gmail.com> wrote:

Hello,

following the recent major changes to our workflow, I will soon turn off the "patchbot server" machine. This will have the side effect of breaking the round "patchbot report" icons in the frozen trac website.

these icons are long gone, already.

 

To people running "patchbot clients", please stop your machines. You may want to turn them to runners in our new setting, but please do not ask me how.

you might want to turn them into runners for GitHub Actions -

https://docs.github.com/en/actions/hosting-your-own-runners/adding-self-hosted-runners

- we can either add them then to our pool of runners (currently we don't have any, we use what's provided by GitHub for free)

- or you can use them to speed up Actions on your GitHub forks of Sage.

Frédéric

--
You received this message because you are subscribed to the Google Groups "sage-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/096df874-34b6-4956-ab53-e249e4d0f658n%40googlegroups.com.