Open lthms opened 3 years ago
About CI, for some reason this project has been somehow split between Travis-ci.com and Travis-ci.org. See:
It turns out that Travis-ci.org is EOL and Travis-ci.com is dead for open source project (see https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users/topic/New.20Travis.20limits.2E, especially my latest update).
I encourage you to switch to GitHub Actions (just change travis: true
into action: true
and regenerate from the templates) when you can.
Thanks for the heads-up. I will try to have a look at this later this week, and hopefully make the switch.
@Zimmi48 there are still some work to do, but I have at least make the switch to Github Actions.
Great! I've pushed a commit to fix the badge in the README.
Thanks! Next time you have to push directly to main
, just try to keep the git message under 72 characters and it would be perfect.
Glad to see this CI things finally moving forward. Having to wait for 30min and more for seeing this green light was a bit annoying.
Sorry about that, and also sorry for the dune-project
issue. I can force-push a fix if you'd like.
If you can squash the two commits and keep the message under 72 characters that would be perfect. Otherwise I can do it later this evening.
Done.