From 6ae1a2df419db8f44e11f5c5d4bb5e387d290a64 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 18 May 2018 02:19:00 -0400
Subject: [doc] Fix some Sphinx LaTeX warnings and silence others

---
 doc/sphinx/conf.py | 1 +
 1 file changed, 1 insertion(+)

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