aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2018-09-12 10:07:56 +0200
committerThéo Zimmermann2018-09-12 10:07:56 +0200
commit701f6ab54498bd5bb3256babe0eb2cb207478b0d (patch)
treef2bddcd1fa3049fbcd7def0d61db508f8a504498
parenta9e0f0ee9e4936d700d39faaa20568c0c561b8fa (diff)
parentd354a29cae28b83dcf4ecb418633b2120211c41a (diff)
Merge PR #8406: building-a-coq-project-with-coq-makefile:fix typos
-rw-r--r--doc/sphinx/practical-tools/utilities.rst15
1 files changed, 8 insertions, 7 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 218a19c2e5..b9a4d2a7bd 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -268,13 +268,12 @@ file timing data:
+ ``print-pretty-timed-diff``
- this target builds a table of timing
- changes between two compilations; run ``make make-pretty-timed-before`` to
- build the log of the “before” times, and run ``make make-pretty-timed-
- after`` to build the log of the “after” times. The table is printed on
- the command line, and stored in ``time-of-build-both.log``. This target is
- most useful for profiling the difference between two commits to a
- repo.
+ this target builds a table of timing changes between two compilations; run
+ ``make make-pretty-timed-before`` to build the log of the “before” times,
+ and run ``make make-pretty-timed-after`` to build the log of the “after”
+ times. The table is printed on the command line, and stored in
+ ``time-of-build-both.log``. This target is most useful for profiling the
+ difference between two commits in a repository.
.. note::
This target requires ``python`` to build the table.
@@ -331,7 +330,9 @@ line timing data:
Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s)
+ ``print-pretty-single-time-diff``
+
::
+
print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing
this target will make a sorted table of the per-line timing differences