#15334 has been merged. We should upstream this at some point to cmdliner in order to address https://github.com/dbuenzli/cmdliner/issues/213. Probably best to give it some time so that we can mature it on our end first.
#15334 has been merged. We should upstream this at some point to cmdliner in order to address dbuenzli/cmdliner#213.
Probably best to give it some time so that we can mature it on our end first.