aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.dev2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev
index 26092e8dc..501a7744a 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -134,7 +134,7 @@ ltac: ltac/ltac.cma
######################
init: $(filter theories/Init/%, $(THEORIESVO))
-logic: $(filter theories/Logic/%, %(THEORIESVO))
+logic: $(filter theories/Logic/%, $(THEORIESVO))
arith: $(filter theories/Arith/%, $(THEORIESVO))
bool: $(filter theories/Bool/%, $(THEORIESVO))
parith: $(filter theories/PArith/%, $(THEORIESVO))