< average vr 56795> ready to merge <https github com pantsbu pantsbuild #development

Channels

github-notifications

Title

# development

w

witty-crayon-22786

04/23/2020, 7:17 PM

@average-vr-56795: ready to merge https://github.com/pantsbuild/pants/pull/9555 ?

a

average-vr-56795

04/23/2020, 7:20 PM

I'm ready if you're happy with the options singleton ness!

Merged :) let's get killing some cruft! :D

w

witty-crayon-22786

04/23/2020, 7:21 PM

hooray 😃

thanks a lot for actually doing that upstream. i know you didn’t need to.