diff options
| author | Jason Gross | 2018-09-05 04:51:40 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-09-11 10:17:19 -0400 |
| commit | d354a29cae28b83dcf4ecb418633b2120211c41a (patch) | |
| tree | aa10a21e7ecd6ea4f0a268dc1c60d10cc0cb3f29 | |
| parent | 053193926ea1397c400355a8d253ec9ba36a5731 (diff) | |
building-a-coq-project-with-coq-makefile:fix typos
make make-pretty-timed- after -> make make-pretty-timed-after (remove
space between - and after) (and reflow paragraph)
Fix spacing around :: in print-pretty-single-time-diff
Closes #8396
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 15 |
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 |
