diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-21 07:53:37 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-21 07:53:37 +0100 |
| commit | d19e5a265cdee251b582792b63ed7e91c313579f (patch) | |
| tree | 563539977ec9ffa3ce845fbf4caa2a4491012804 /.gitlab-ci.yml | |
| parent | 3ad897c65d5f16159694ede55958ac8c85339d55 (diff) | |
| download | compcert-kvx-d19e5a265cdee251b582792b63ed7e91c313579f.tar.gz compcert-kvx-d19e5a265cdee251b582792b63ed7e91c313579f.zip | |
tentative pour n'avoir le gitlab-ci que sur mppa-work, mppa-k1c et master
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b4571271..79a00d3b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -11,6 +11,10 @@ build_x86_64: script: - ./config_x86_64.sh - make -j "$NJOBS" + only: + - master + - mppa-k1c + - mppa-work build_ia32: stage: build @@ -22,6 +26,10 @@ build_ia32: script: - ./config_ia32.sh - make -j "$NJOBS" + only: + - master + - mppa-k1c + - mppa-work build_aarch64: stage: build @@ -35,6 +43,10 @@ build_aarch64: script: - ./config_aarch64.sh - make -j "$NJOBS" + only: + - master + - mppa-k1c + - mppa-work build_arm: stage: build @@ -48,6 +60,10 @@ build_arm: script: - ./config_arm.sh - make -j "$NJOBS" + only: + - master + - mppa-k1c + - mppa-work build_ppc: stage: build @@ -61,6 +77,10 @@ build_ppc: script: - ./config_ppc.sh - make -j "$NJOBS" + only: + - master + - mppa-k1c + - mppa-work build_rv64: stage: build @@ -74,6 +94,10 @@ build_rv64: script: - ./config_rv64.sh - make -j "$NJOBS" + only: + - master + - mppa-k1c + - mppa-work build_rv32: stage: build @@ -87,6 +111,10 @@ build_rv32: script: - ./config_rv32.sh -no-runtime-lib - make -j "$NJOBS" + only: + - master + - mppa-k1c + - mppa-work build_k1c: stage: build @@ -98,3 +126,6 @@ build_k1c: script: - ./config_k1c.sh -no-runtime-lib - make -j "$NJOBS" + only: + - mppa-k1c + - mppa-work |