diff options
| author | Jason Gross | 2020-02-06 23:14:33 -0500 |
|---|---|---|
| committer | GitHub | 2020-02-06 23:14:33 -0500 |
| commit | 53f6560f766fdbb7176eb7247c712c690f4a6f1f (patch) | |
| tree | e1c5020609f3aa1c5581b8380bd3056f0d103e57 | |
| parent | 6799ad6240fa4d233f698c3cfa0bd5417f471bba (diff) | |
Apply suggestions from code review
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 64a4716188..24b766b204 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -264,7 +264,7 @@ file timing data: ``run make cleanall``. .. note:: - By default the table picks up user times. If the build log + By default the table displays user times. If the build log contains real times (which it does by default), passing ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times rather than user times in the table. @@ -387,7 +387,7 @@ line timing data: .. note:: By default, two lines are only considered the same if the - character offsets and initial code strings match. Passing + character offsets and initial code strings are identical. Passing ``TIMING_FUZZ=N`` relaxes this constraint by allowing the character offsets to differ by up to ``N`` characters, as long as the total number of characters and initial code strings |