aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Ralf Jung <post@ralfj.de>2018-03-21 19:40:30 +0100
committerGravatar Ralf Jung <post@ralfj.de>2018-03-21 19:40:30 +0100
commitc0e34f2700f769e87f1449ae27b20e0d0546aec7 (patch)
tree09ff7c54cf9b2cb84501fb4da2ae69869a29a9e6 /tools
parentb716378fce3611d06060c4f71da4b6d87f89c09c (diff)
docs
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in6
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 7bcc340ac..f6539d80b 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -148,7 +148,11 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
# Flags #######################################################################
#
-# We define a bunch of variables combining the parameters
+# We define a bunch of variables combining the parameters.
+# To add additional flags to coq, coqchk or coqdoc, set the
+# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add.
+# To overwrite the default choice and set your own flags entirely, set the
+# {COQ,COQCHK,COQDOC}FLAGS variable.
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)