diff options
| author | Théo Zimmermann | 2018-07-27 15:48:21 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-27 15:48:21 +0200 |
| commit | 941b25c8617d88bdf128379f98f443cc46d6ffcc (patch) | |
| tree | 1dc9b3f535dec71f0227152c74217657b15919bc | |
| parent | 05ef2d2234578294cd0be6aace2b4ed4c9815d37 (diff) | |
| parent | 05685d54fb5b737252047cd0ca9f646acf1d13f5 (diff) | |
Merge PR #8173: Missing backslash in a documentation file.
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index bdaa2aa1a2..e15bcb8e2c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -546,12 +546,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. |