diff options
| author | Théo Zimmermann | 2020-06-10 15:45:15 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-10 17:04:58 +0200 |
| commit | ba8c793ed4947b04ee3f8157e8a3d1dd8d529eeb (patch) | |
| tree | ad66c3fffa90a53bdf58140214ec63e7946117a8 /dev/build | |
| parent | e2afb5b493612e96e0c86e769d9486486494580c (diff) | |
Fix the build of Elpi by calling Dune directly.
Diffstat (limited to 'dev/build')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fca8cd6120..6ceb7f54b2 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1193,10 +1193,10 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz; then + if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then - log2 make build DUNE_OPTS="-p elpi" - log2 make install DUNE_OPTS="-p elpi" + log2 dune build -p elpi + log2 dune install elpi build_post |