Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
In principle, the second command is not needed since coq-bot already depends on bot-components. Furthermore, since a few days, this second command seems to consistently trigger a timeout in our CI during the Docker build. So removing it could help fix this issue.
- Loading branch information