<@U6YPB4SJX>: ready to merge <https://github.com/p...
# developmentw
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 PMI'm ready if you're happy with the options singleton ness!
average-vr-56795
04/23/2020, 7:21 PMMerged :) let's get killing some cruft! :D
w
witty-crayon-22786
04/23/2020, 7:21 PMhooray 😃
witty-crayon-22786
04/23/2020, 7:21 PMthanks a lot for actually doing that upstream. i know you didn’t need to.