Closed asonnino closed 11 months ago
The first commit (Do not wait for dead leaders) looks good, and it passes the checks - I think we can cherry-pick it to the main branch. For other commits we would need to pass the checks first (and ideally merge them as separate PRs / main branch commits since they are very different
The first commit (Do not wait for dead leaders) looks good, and it passes the checks - I think we can cherry-pick it to the main branch. For other commits we would need to pass the checks first (and ideally merge them as separate PRs / main branch commits since they are very different
ah I didn't notice it didn't pass the checks. I plan to merge this branch into paper
rather than main
since we are a bit rushing for the deadline