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
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: Feb 06 2023 at 00:03 UTC