diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-27 14:44:15 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-28 12:57:28 +0100 |
| commit | b16f9e8a17d2223e6045e57a11bef2aa44ffb6ff (patch) | |
| tree | c5b87ec42015910929d4f86e0f1ef3d6eca83f25 /Makefile.dev | |
| parent | 79810d6665be221bb35e131a453fcd4010580ebb (diff) | |
CI: use -byte-only in [warnings] jobs.
This avoids mixing native and byte compilation as the debug printers
are always byte compiled and the tools have no .byte rule, only the
OCAMLBEST rule.
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 dc4ded397..d2a1e9235 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 |