9 months later, this PR is still open. to record my vote: -1

[dimpase]

9 months later, this PR is still open.

The current tally:

• 4 in favor: @mkoeppe @kwankyu @kiwifb @NathanDunfield
• 4 against: @tobiasdiez @tornaria @orlitzky @saraedum

Please vote!

Originally posted by @mkoeppe in #36561 (comment)

[orlitzky]

Obsolete, thankfully.