aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Yannick Forster <forster@ps.uni-saarland.de>2018-02-07 10:47:59 +0100
committerGravatar Yannick Forster <forster@ps.uni-saarland.de>2018-02-07 10:47:59 +0100
commitf4936d8512c9035e0628f22c08d576ea9ef62ad0 (patch)
tree70c3e11676fb03a3c52f5ad470d472e93c4a725a /tools
parentb1d56e48b2453814a5d2898688fbc7c5d29d32fa (diff)
Possible fix for issue #6697
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in3
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index ca02c983d..173eaae89 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -169,7 +169,8 @@ endif
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
COQCHKFLAGS?=-silent -o $(COQLIBS)
-COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
+COQDOCFLAGS?=-interpolate -utf8
+COQDOCLIBS?=$(COQLIBS_NOML)
# The version of Coq being run and the version of coq_makefile that
# generated this makefile