From b16f9e8a17d2223e6045e57a11bef2aa44ffb6ff Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 27 Nov 2017 14:44:15 +0100
Subject: 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.
---
 Makefile.dev | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.dev')

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
 
-- 
cgit v1.2.3