There have been a few requests in recent years for a more "active" bot for various repository actions to be triggered via a GitHub comment. The current requests are:
for opam-repository maintainers to have more control over whether certain expensive tests are run, for example reverse dependencies on popular packages like dune that trigger a lot of builds.
There have been a few requests in recent years for a more "active" bot for various repository actions to be triggered via a GitHub comment. The current requests are:
dune
that trigger a lot of builds.There are a couple of workflow mechanisms we can use for this, possibly in combination:
We already have several GitHub bot accounts that are suitable for use as a host for this: @bactrian and @vicuna.
This is a tracking issue for the deployment and maintainence of such a bot once the prototypes have been completed.