Hey folks I'm awake again and have shepherded some MRs ready to merge: • https://github.com/pantsbuild/pants/pull/20788 • https://github.com/pantsbuild/pants/pull/20787 • https://github.com/pantsbuild/pants/pull/20764

I forget who has merge privs or not. Do you need someone to merge these?

yes please

done