aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-05-30 10:54:03 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-05-31 10:04:30 +0200
commit5e7d5491304ce3765fa245bb697a239b05921636 (patch)
tree1434d6e347c4648fbcfcfccd349b950af6adf587
parent71004fe0ab615da7e5fd6cd5634253e3cc43eae2 (diff)
removing duplicate line from "tools/CoqMakefile.in"
-rw-r--r--tools/CoqMakefile.in1
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fb064c495..13a57a37d 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@