From 5e7d5491304ce3765fa245bb697a239b05921636 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Tue, 30 May 2017 10:54:03 +0200
Subject: removing duplicate line from "tools/CoqMakefile.in"

---
 tools/CoqMakefile.in | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fb064c495f..13a57a37dc 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -39,7 +39,6 @@ CAMLP4BIN         := $(COQMF_CAMLP4BIN)
 CAMLP4LIB         := $(COQMF_CAMLP4LIB)
 CAMLP4OPTIONS     := $(COQMF_CAMLP4OPTIONS)
 HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
-COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
 
 @CONF_FILE@: @PROJECT_FILE@
 	@COQ_MAKEFILE_INVOCATION@
-- 
cgit v1.2.3