diff options
| author | Clément Pit-Claudel | 2018-05-18 02:19:00 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | 6ae1a2df419db8f44e11f5c5d4bb5e387d290a64 (patch) | |
| tree | 30f4fdd3417a3c2c71f11d1c5000d3be26997ce8 | |
| parent | fdc5e750f7b87c1d0d1454bae19c00eec9dabbeb (diff) | |
[doc] Fix some Sphinx LaTeX warnings and silence others
| -rwxr-xr-x | doc/sphinx/conf.py | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index b85cf57a98..143309fab5 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -166,6 +166,7 @@ primary_domain = 'coq' # The name of the Pygments (syntax highlighting) style to use. pygments_style = 'sphinx' highlight_language = 'text' +suppress_warnings = ["misc.highlighting_failure"] # A list of ignored prefixes for module index sorting. #modindex_common_prefix = [] |