<!-- Thank you for your contribution.
     Make sure you read the contributing guide and fill this template. -->


<!-- Keep what applies -->
**Kind:** documentation / bug fix / feature / performance / infrastructure.


<!-- If this is a bug fix, make sure the bug was reported beforehand. -->
Fixes / closes #????


<!-- If there is a user-visible change in coqc/coqtop/coqchk/coq_makefile behavior and testing is not prohibitively expensive: -->
<!-- (Otherwise, remove this line.) -->
- [ ] Added / updated test-suite
<!-- If this is a feature pull request / breaks compatibility: -->
<!-- (Otherwise, remove these lines.) -->
- [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
- [ ] Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).
- [ ] Overlay pull requests (if this breaks 3rd party developments in CI, see
https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md for details)