diff options
| -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:: |