From 05685d54fb5b737252047cd0ca9f646acf1d13f5 Mon Sep 17 00:00:00 2001
From: Martin Bodin
Date: Fri, 27 Jul 2018 11:52:15 +0100
Subject: Missing backslash in the documentation file.

---
 doc/sphinx/practical-tools/utilities.rst | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'doc')

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.
-- 
cgit v1.2.3