[CI failure] Fix bad interaction between merging of #13664 and #14598

[proux01]

We should have rerun CI before merging #13664, this would have avoided
missing that #13664 forgot to take #14598 into account.

This should fix the test-suite jobs in the CI that are broken since the merging of #13664

[coqbot-app]

Hey, I have detected that there were CI failures at commit e63ee29 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 6bd07ba succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize all, I will additionally minimize the following target (which I do not suggest minimizing): ci-category_theory (because base job at 6bd07ba failed)

[ppedrot]

That's a duplicate of #14834 but since I have merge rights, that nobody cared about the other one and that fixing the test-suite is urgent, I'll merge this right now and close the other one.

[proux01]

@ppedrot sorry, I somehow missed #14834 (and I don't (yet) have merge rights anyway ;) )
Well, thanks for merging!