diff options
| author | Sébastien Hinderer <Sebastien.Hinderer@inria.fr> | 2021-10-04 11:26:15 +0200 |
|---|---|---|
| committer | Sébastien Hinderer <Sebastien.Hinderer@inria.fr> | 2021-10-04 11:26:15 +0200 |
| commit | 8f713c59f7732d1547e06eea5775b42c9ea56da7 (patch) | |
| tree | bf68f12788861392bfa1e660699fe4002c53584e /tools | |
| parent | 3eb0ab091f83b6d769ba6463a718b6935b011bc5 (diff) | |
| download | ocaml-8f713c59f7732d1547e06eea5775b42c9ea56da7.tar.gz | |
Fix script for Inria's other-configs CI job
This commit contains two fixes:
1. Remove a superfluous occurence of "-conf --disable-native-compiler"
(passed twice)
2. Remove the "-no-native" option which is no longer necessary.
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/inria/other-configs/script | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tools/ci/inria/other-configs/script b/tools/ci/inria/other-configs/script index c3279f63cf..626d7d1dd1 100755 --- a/tools/ci/inria/other-configs/script +++ b/tools/ci/inria/other-configs/script @@ -36,9 +36,7 @@ ${main} -conf --disable-native-compiler \ -conf --disable-unix-lib \ -conf --disable-bigarray-lib \ -conf --disable-ocamldoc \ - -conf --disable-native-compiler \ - -conf --disable-dependency-generation \ - -no-native + -conf --disable-dependency-generation ${main} -conf --disable-naked-pointers ${main} -with-bootstrap -conf --disable-flat-float-array ${main} -conf --enable-flambda -conf --disable-naked-pointers |