Stream: Coq devs & plugin devs

Topic: pipeline list


view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 09:02 UTC