diff options
author | Matej Košík <matej.kosik@inria.fr> | 2017-05-30 10:54:03 +0200 |
---|---|---|
committer | Matej Košík <matej.kosik@inria.fr> | 2017-05-31 10:04:30 +0200 |
commit | 5e7d5491304ce3765fa245bb697a239b05921636 (patch) | |
tree | 1434d6e347c4648fbcfcfccd349b950af6adf587 | |
parent | 71004fe0ab615da7e5fd6cd5634253e3cc43eae2 (diff) |
removing duplicate line from "tools/CoqMakefile.in"
-rw-r--r-- | tools/CoqMakefile.in | 1 |
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@ |