aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev
index 9659f602d7..13b85dfad4 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -63,7 +63,7 @@ revision:
coqlight: theories-light tools coqbinaries
-states: theories/Init/Prelude.vo
+states: theories/Init/Prelude.$(VO)
miniopt: $(COQTOPEXE) pluginsopt
minibyte: $(COQTOPBYTE) pluginsbyte