Closed ppedrot closed 2 weeks ago
Gah, there are still users of that crap in the wild...
The itauto plugin depends on that code only through dead code: https://gitlab.inria.fr/fbesson/itauto/-/merge_requests/16.
@SkySkimmer ci green now.
@coqbot merge now
It was deprecated since 8.16.