diff options
| author | Pierre-Marie Pédrot | 2020-03-31 00:48:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-31 00:48:42 +0200 |
| commit | e2f0814688511be93659c2258b91248698f18d4a (patch) | |
| tree | 06c1860a6e5b45ee154e45bfbddfff228ac22cdd /.gitlab-ci.yml | |
| parent | 8c85a8651605dd82ce2223a28ca38f31359a88bd (diff) | |
| parent | 5c9f318f5f1b6e85b03bba9450ac059377be54fc (diff) | |
Merge PR #11647: [rfc] Consolidation of parsing interfaces
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 39c801197b..f2e0c362b4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -103,6 +103,9 @@ before_script: interruptible: true dependencies: [] script: + # flambda can be pretty stack hungry, specially with -O3 + # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244 + - ulimit -s 16384 - set -e - make -f Makefile.dune world - set +e |