diff options
Diffstat (limited to 'dev')
| -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 |