diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 21:57:46 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:41:23 -0400 |
| commit | 4a88beff476d2c27eae381bc8a61f777015c0617 (patch) | |
| tree | e472daac96fc2086486db89d57b62550e3c1c572 | |
| parent | 1217583de0c7ac0d17c8917f21c30c247176d83f (diff) | |
[gitlab] Increase flambda stack size.
See https://github.com/ocaml/ocaml/issues/7842
| -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 ebeee0d4e4..df71ab3c2f 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 |