diff options
| author | Antonio Nikishaev | 2019-09-27 06:16:40 +0300 |
|---|---|---|
| committer | Antonio Nikishaev | 2019-10-22 23:38:28 +0400 |
| commit | 395519de374e2c51cde2b2777af90f8af1200ea2 (patch) | |
| tree | 09ef9feb847988b05f24c79f1e16b480a0bdaf30 /doc/sphinx/practical-tools | |
| parent | 54689c1c1e1333dd1bf63c619481c2ec99a5762e (diff) | |
documentation fixes
document « Property »
more documentation fixes
[doc] destructed → destructured
[doc] another le_minus→lt_1_r
[doc] @jfehrle suggestions
[doc] more minor fixes
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 9e219bd503..e5edd08995 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -359,7 +359,7 @@ line timing data: pass ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``. .. note:: - The sorting used here is the same as in the ``print-pretty-timed -diff`` target. + The sorting used here is the same as in the ``print-pretty-timed-diff`` target. .. note:: This target requires python to build the table. |