aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-16 13:05:25 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-07-11 05:32:56 -0400
commit097dd1c608dd7c375d159301af5fb9bf37445d9a (patch)
tree9eb33de22c732c3963c4dc4d84ac371025d2d7b8 /CHANGES
parent62b8d99f1430a8a477d36be86d91aba8807659db (diff)
Add an entry to CHANGES about timing in coq_makefile
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES5
1 files changed, 5 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 4e95f9d4c..91abaa10b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -95,6 +95,11 @@ Tools
The current version contains code for retro compatibility that prints
warnings when a deprecated feature is used. Please upgrade your _CoqProject
accordingly.
+ * Additionally, coq_makefile-made Makefiles now support experimental timing
+ targets `pretty-timed`, `pretty-timed-before`, `pretty-timed-after`,
+ `print-pretty-timed-diff`, `print-pretty-single-time-diff`,
+ `all.timing.diff`, and the variable `TIMING=1` (or `TIMING=before` or
+ `TIMING=after`); see the documentation for more details.
Build Infrastructure