aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Ralf Jung <post@ralfj.de>2018-04-16 10:44:44 +0200
committerGravatar Ralf Jung <post@ralfj.de>2018-04-16 10:44:44 +0200
commit573241e4edcf3d0217718679847192cdaadf5de8 (patch)
tree815b26db6839cd9085ce5f71d1b2f51fe5406498 /CHANGES
parent8fdfbdbcb4156571a43db7445dea6cd6cec58a53 (diff)
CHANGES: document COQFLAGS change
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 06a9bba7d..40e8547ae 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,8 @@ Tools
- Coq_makefile lets one override or extend the following variables from
the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS.
+ COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles
+ $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS).
Vernacular Commands