Hi folks, what do you think about changing the
kind: infrastructure tag to
part: infra ?
Actually that'd work better in terms of
part: infrastructure being almost covered by
part: build, etc...
What is the reason?
"kind: " today has a special status for coq/bot for instance.
kind: is a mandatory label category to merge a PR. If we remove it (e.g., in favor of
part: build, etc.), this means that we have to always add another
kind: label, such as
kind: fix. And it's often the case that we don't want to qualify infrastructure work as such IINM...
Good point @Théo Zimmermann , what would be an example of such a change?
part: X vs
kind: A is about "action A on object X"
kind: internal and
kind: cleanup tho
Indeed. I agree in principle with your interpretation and that we are not always consistent.
I wouldn't object to revisiting the labels, even if it requires adapting coqbot BTW.
Does coqbot care about
kind: infra ? As far as I know is the only label that seems wrong
At least that's the one I feel most out of sync, the rest of kind seem logical to me
kind: infrastructure specifically is also special as it deactivates minimization.
Last updated: Dec 06 2023 at 13:01 UTC