diff options
| author | Théo Zimmermann | 2019-02-05 09:49:54 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-05 09:49:54 +0100 |
| commit | 740ec848acc0b127fad7ba5b703bc00364126c71 (patch) | |
| tree | d72ced5aaa9d4b4ba3061e649a0e9462f238b5a0 /Makefile.dune | |
| parent | 5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff) | |
| parent | 0439543db9f3be84d59cfdc1dcad34bd114036e3 (diff) | |
Merge PR #8421: [dune] Fix Dune build in Windows.
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index ee3e2d6cb7..78ecc4b056 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -40,7 +40,7 @@ help: voboot: dune build $(DUNEOPT) @vodeps - dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d + dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d states: voboot dune build $(DUNEOPT) theories/Init/Prelude.vo |