On 10 April 2024 03:39:00 CEST, Kwankyu Lee <ekwan...@gmail.com> wrote:
>How about redefining the meaning of "CI Fix" label:
>
>1. We designate a person to be the CI manager.
>2. For PRs pertaining to the designated directories and files, we add "CI
>Fix" label
>3. The CI manager has the right to merge PRs with "CI Fix" label to develop.
>4. The old meaning of "CI Fix" label as "immediate fixes" is dropped.
>5. Hot fix PRs for breakage of CI also gets "CI Fix" label.
No, this has a big risk that such a manager will accidentally push non-CI bits,
and obviously the discipline for not mixing CI and non-CI bits in one commit/PR
will need to be manually managed.
This is why my proposal to split the repo is much better in this way.
(One of the mottos of the political party I am forced to set up is "monorepos
considered harmful", along with "batteries excluded" :-))
>
>?
>
>
--
You received this message because you are subscribed to the Google Groups
"sage-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to sage-devel+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/sage-devel/2F5FD23C-680E-4FC5-8ECE-69BE08A3F3B0%40gmail.com.
