diff options
Diffstat (limited to 'doc/sphinx/conf.py')
| -rwxr-xr-x | doc/sphinx/conf.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index d98b8641e9..e681d0f3ff 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -147,7 +147,7 @@ exclude_patterns = [ # The reST default role (used for this markup: `text`) to use for all # documents. -#default_role = None +default_role = 'literal' # Use the Coq domain primary_domain = 'coq' |