diff options
| author | Maxime Dénès | 2017-12-01 09:30:14 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-01 09:30:14 +0100 |
| commit | 565c2c2a56e118d9cf9b6b72b623055bcd68af60 (patch) | |
| tree | ec9267a3d090a256d859b6f1bf4f0ced0b09c5fd /Makefile.dev | |
| parent | 317a47249e666e2e11c6a8ac29f7c8370c861f8a (diff) | |
| parent | b16f9e8a17d2223e6045e57a11bef2aa44ffb6ff (diff) | |
Merge PR #6256: CI: better ocaml warning checks
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev index dc4ded3977..d2a1e9235e 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -98,7 +98,7 @@ pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) # This should build all the ocaml code but not (most of) the .v files -coqocaml: tools coqbinaries pluginsopt coqide printers bin/votour +coqocaml: tools coqbinaries $(PLUGINSCMO:.cmo=$(DYNOBJ)) coqide printers bin/votour .PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml |