aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-13 09:45:41 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-13 09:45:41 +0200
commit3f9215b2b65b902cc52fd540f57f67342401a91f (patch)
tree98191563b3c42ce4e5c559039de380c0d00ac227 /Makefile.dev
parent605048905db9107a1d4b3c35ce59f5719474f875 (diff)
Makefile.dev: fix a typo in the 'logic' rule
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 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))