aboutsummaryrefslogtreecommitdiffstats
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-23 18:40:19 +0200
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-23 18:40:19 +0200
commit749d2beee61986a3464d81cd84097fbffe4affff (patch)
tree03c0fa35fa4015916c09914788ca8acb0086f760 /.gitlab-ci.yml
parent87e3508310e3e312e26f7d69357289a99242e243 (diff)
downloadcompcert-kvx-749d2beee61986a3464d81cd84097fbffe4affff.tar.gz
compcert-kvx-749d2beee61986a3464d81cd84097fbffe4affff.zip
rm spurious comment
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 69965541..72125292 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -220,7 +220,6 @@ build_rv64:
- make -j "$NJOBS"
- make -C test SIMU='qemu-riscv64 -L /usr/riscv64-linux-gnu' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu' all test
- ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu'
- # disabled until https://github.com/AbsInt/CompCert/issues/412 is fixed
- ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='timeout 10s qemu-riscv64 -L /usr/riscv64-linux-gnu' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
rules:
- if: '$CI_COMMIT_BRANCH == "kvx-work"'