<@U02RUEH9C1L> I'm willing to merge <https://githu...
# development
p
@witty-family-13337 I'm willing to merge https://github.com/pantsbuild/pants/pull/15638/ , but it's been awhile since you wrote this. Do you have anything else you want to do with it or just merge it?