Closed proux01 closed 7 months ago
Needed for https://github.com/math-comp/math-comp/pull/1201
@pi8027 could you please merge this trivial one?
Thanks
Needed for https://github.com/math-comp/math-comp/pull/1201