aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build
index ffe605757..179ca28b6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -89,6 +89,7 @@ byte: coqbyte coqide-byte pluginsbyte printers
MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
include Makefile.common
+include Makefile.vofiles
include Makefile.doc ## provides the 'documentation' rule
include Makefile.checker
include Makefile.ide ## provides the 'coqide' rule