Fix CI DEFAULT branch after bad merge/revert in stable

506e66c5 · François Bobot · 591e456f · 506e66c5
Commit 506e66c5 authored 2 years ago by François Bobot
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -7,7 +7,7 @@ stages:

 variables:
    CURRENT: $CI_COMMIT_REF_NAME
-    DEFAULT: "stable/manganese"
+    DEFAULT: "master"
    FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
    OCAML: "4_08"