|
From: Peter Da S. <pet...@fl...> - 2023-05-12 01:10:21
|
> A vote could be not on a formal TIP, but on a request to merge a > particular commit (not a branch, but a specific commit), complete with > correct documentation relevant to the change. Why a commit rather than a branch? And would it be merged by cherry-pick if there is more than one commit in the pull request? What if additional changes are made after the commit, as a result of discussion, as there are for TIPs? |