From c0e34f2700f769e87f1449ae27b20e0d0546aec7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 21 Mar 2018 19:40:30 +0100
Subject: docs

---
 tools/CoqMakefile.in | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'tools')

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),,@)
-- 
cgit v1.2.3