From 37b900aeda68ae1e067a7770c16c11ea327a14dc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 6 Feb 2019 11:09:04 +0100
Subject: Fix #9486: Makefile.install should not have a target foo

---
 Makefile.install | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Makefile.install b/Makefile.install
index b6e2ec2aeb..f289442aea 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -100,9 +100,6 @@ INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
 	configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \
 	$(filter %.cmx, $(GRAMMLFILES:.ml=.cmx)) $(MLFILES:.ml=.cmx)))
 
-foo:
-	@echo $(INSTALLCMX)
-
 install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)
-- 
cgit v1.2.3