coqdoc: Report location of mismatched '[['

coq · Apr 10, 2020 · 41a1d66 · 41a1d66
1 parent 1d7729c
commit 41a1d66
Show file tree

Hide file tree

Showing 2 changed files with 151 additions and 87 deletions.
diff --git a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  ``coqdoc`` now reports the location of a mismatched opening ``[[`` instead of
+  throwing an uninformative exception.
+  (`#12037 <https://github.com/coq/coq/pull/12037>`_,
+  fixes `#9670 <https://github.com/coq/coq/issues/9670>`_,
+  by Lysxia).