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 68e96a57b7..7fc1076a8f 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -91,7 +91,7 @@ endif
coqlight: theories-light tools coqbinaries
-states: camldevfiles theories/Init/Prelude.vo
+states: theories/Init/Prelude.vo
miniopt: $(COQTOPEXE) pluginsopt
minibyte: $(COQTOPBYTE) pluginsbyte