diff options
| author | Jason Gross | 2020-02-14 17:26:49 -0500 |
|---|---|---|
| committer | GitHub | 2020-02-14 17:26:49 -0500 |
| commit | f9928b83a2e2eda7bbb9cd7fac0ea6e1ef1be30f (patch) | |
| tree | b620d41c8e53267934a8e06fad4828061df409e1 /doc/sphinx | |
| parent | 82ab894460fb25d85acf8c4ce0d177ecc4dbfd86 (diff) | |
Apply suggestions from code review
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 626a658b6c..23b7dcfeba 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -323,8 +323,7 @@ file timing data: .. note:: Just like ``pretty-timed``, this table defaults to using user - times and supports ``TIMING_REAL=1`` to specify that real times - rather than user times should be used. + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. .. example:: |