> - This creates an immediate need to modify the PR merge script; Raúl > opened an issue for this after the call [6]; this also raises the > question of whether we still need the PR merge script or whether > committers can use the "Squash and merge" button in the GitHub web UI > instead >
I think the only thing the merge script will do better than the UI button is that the script always gets the merge commit title correct. IIRC in the GitHub UI, if you merge a PR that has only one commit, it uses the commit message from that commit and not the PR title. Maybe GitHub has fixed this (or let it be configurable). How do apache/arrow-rs, arrow-datafusion, arrow-julia, et al. handle this? Neal
