diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-01-19 11:19:02 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-01-19 11:19:02 +0100 |
| commit | 259afac999e9cacd9203f62b816f14ad5a82ae50 (patch) | |
| tree | 72bece45f281c14953fd30c1d456c54ae388c70f /tools | |
| parent | 00fce0b9b896d5d81f3d3a127ecc54edc5cdf9da (diff) | |
| download | ocaml-259afac999e9cacd9203f62b816f14ad5a82ae50.tar.gz | |
Enable flambda only if actually requested
Currently, when this script is called from the other-configs script,
the flambda environment variable is not set, and
`if $flambda; then ...` takes the `then` branch, activating flambda.
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/inria/main | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/ci/inria/main b/tools/ci/inria/main index 49753d0741..7a6232c19b 100755 --- a/tools/ci/inria/main +++ b/tools/ci/inria/main @@ -238,7 +238,7 @@ export LC_ALL=C git clean -q -f -d -x -if $flambda; then +if test "$flambda" = "true"; then confoptions="$confoptions --enable-flambda --enable-flambda-invariants" fi |