Gaëtan Gilbert (Oct 23 2022 at 15:47): Gaëtan Gilbert (Oct 23 2022 at 15:47):I wonder if we could make it easier to tell which pipelines are full/light in the list https://gitlab.com/coq/coq/-/pipelines
importing the list into something that has better search would be nice too
Théo Zimmermann (Oct 24 2022 at 09:21):Since the ci merge commit is usually created by coqbot when it has the info whether this will be a full or light pipeline, we could consider adding the info somewhere toward the beginning of the commit message. This could of course lead to false information in case someone manually starts a pipeline using the GitLab UI (but I don't think it happens much these days).
Last updated: Jun 05 2023 at 10:01 UTC