| Age | Commit message (Collapse) | Author |
|---|
|
GitLab setup is quite stable these days thanks to the work of many
people and `coqbot`. We decided to keep CircleCI support for a while
as a safeguard in case something happened in the migration to GitLab,
but these days we are just wasting resources to them and to us. As I'm
afraid CircleCI won't scale for us, the time to remove it has arrived.
Still, CircleCI had some awesome functionality that GitLab's CI
doesn't offer yet, see the links at:
https://github.com/coq/coq/issues/6919#issuecomment-395885573
- https://gitlab.com/gitlab-org/gitlab-ce/issues/29347
- https://gitlab.com/gitlab-org/gitlab-ce/issues/35222
- https://gitlab.com/gitlab-org/gitlab-ce/issues/41947
- https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
|
|
We are now actively looking for sponsors, let's make our communication
more visible.
|
|
This will avoid in particular this ambiguous file extension.
[ci skip]
|
|
We had mostly used absolute links in the past.
I just discovered that GitHub recommends using relative links instead:
https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links
and indeed my Emacs Markdown mode can handle relative links but doesn't
interpret absolute links relatively to the root of the git repository.
[ci skip]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit adds an issue template asking for version and OS information
and adapts the contributing guide to the change of bug tracker.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
