diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index bdaa2aa1a2..59bc2d22aa 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -218,6 +218,7 @@ file timing data: On ``Mac OS``, this works best if you’ve installed ``gnu-time``. .. example:: + For example, the output of ``make TIMED=1`` may look like this: @@ -295,6 +296,7 @@ file timing data: files which take effectively no time to compile. .. example:: + For example, the output table from ``make print-pretty-timed-diff`` may look like this: @@ -318,6 +320,7 @@ line timing data: line-by-line timing information. .. example:: + For example, running ``make all TIMING=1`` may result in a file like this: :: @@ -345,6 +348,7 @@ line timing data: This target requires python to build the table. .. example:: + For example, running ``print-pretty-single-time-diff`` might give a table like this: :: @@ -546,12 +550,12 @@ The printing for one token can be removed with Initially, the pretty-printing table contains the following mapping: -==== === ==== ===== === ==== ==== === -`->` → `<-` ← `*` × -`<=` ≤ `>=` ≥ `=>` ⇒ -`<>` ≠ `<->` ↔ `|-` ⊢ -`\/` ∨ `/\\` ∧ `~` ¬ -==== === ==== ===== === ==== ==== === +===== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\\/` ∨ `/\\` ∧ `~` ¬ +===== === ==== ===== === ==== ==== === Any of these can be overwritten or suppressed using the printing commands. |