Skip to content
Snippets Groups Projects
  1. Feb 15, 2025
  2. Dec 30, 2024
  3. Dec 29, 2024
  4. Dec 18, 2024
  5. Dec 16, 2024
  6. Dec 15, 2024
  7. Dec 14, 2024
  8. Dec 13, 2024
  9. Dec 12, 2024
  10. Dec 11, 2024
  11. Dec 10, 2024
  12. Dec 04, 2024
  13. Dec 03, 2024
  14. Dec 02, 2024
    • Carsten Gräser's avatar
      [ci] Make .gitlab-ci.yml portable · 70bcdbdf
      Carsten Gräser authored
      Currently the CI config requires that the `core/ci-config`
      project exists on the same gitlab server. This prevents
      the CI from working when pushing the repository to another
      server. While one may argue, that one also has to push
      `core/ci-config` then, it is a very strong restriction to
      require that the gitlab group `core` is available.
      
      This can be avoided by using a gitlab remote include for those
      files with a link pointing to the dune server instead of a local
      include.
      70bcdbdf
  15. Nov 29, 2024
Loading