Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • C coq
  • Project information
    • Project information
    • Activity
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
  • Activity
  • Graph
  • Commits
Collapse sidebar
  • coq
  • coq
  • Repository
  • coq
  • README.md
Find file BlameHistoryPermalink
  • Emilio Jesus Gallego Arias's avatar
    [ci] Remove CircleCI setup. · dfafe315
    Emilio Jesus Gallego Arias authored Jul 27, 2018
    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
    dfafe315