Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Browse files
Browse the repository at this point in the history
We should have rerun CI before merging coq#13664, this would have avoided missing that coq#13664 forgot to take coq#14598 into account.
- Loading branch information