From 7217d14466bf900ec0353b6bbcb7e4d4b78ec2bf Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Wed, 13 Jul 2016 09:45:41 +0200
Subject: Makefile.dev: fix a typo in the 'logic' rule

---
 Makefile.dev | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.dev')

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))
-- 
cgit v1.2.3