From d9209353ced1b6ba23cb18e6b4d8e8f9c0c20d92 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Thu, 17 May 2018 22:22:10 -0400
Subject: [doc] Fix a typo in the developer guide

---
 doc/tools/coqrst/coqdomain.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools')

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index f62df94e36..3bb805f2dc 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -496,7 +496,7 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
 CoqCodeRole = coq_code_role
 
 class CoqtopDirective(Directive):
-    """A reST directive to describe interactions with Coqtop.
+    r"""A reST directive to describe interactions with Coqtop.
 
     Usage::
 
-- 
cgit v1.2.3