diff options
| author | Thomas Letan | 2020-07-29 14:53:19 +0200 |
|---|---|---|
| committer | Thomas Letan | 2020-07-29 17:48:22 +0200 |
| commit | ce233d5b4a6f8d506c37a2a492679a66f9618a94 (patch) | |
| tree | 6e3397d7820edfe44c6266d0ff613ff5c2871e45 /doc | |
| parent | 827d430fc5645bf5ad12d0a7fc6298b56ccce5f0 (diff) | |
coqdoc: Fix the “details” environment
The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/12772-fix-details.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst new file mode 100644 index 0000000000..67ee061285 --- /dev/null +++ b/doc/changelog/08-tools/12772-fix-details.rst @@ -0,0 +1,5 @@ +- **Fixed:** + The `details` environment added in the 8.12 release can now be used + as advertised in the reference manual + (`#12772 <https://github.com/coq/coq/pull/12772>`_, + by Thomas Letan). |