aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-07-16 15:26:59 +0200
committerEmilio Jesus Gallego Arias2020-07-16 15:26:59 +0200
commitf54bc666c62ad9a66067cb486816cdfc68c2946d (patch)
tree3e6b02e8874778411765c161384b2bf6dc25b12c /doc
parent3eccf67b2e4aed36fc6935900167b19bcf6dffde (diff)
parente52f070515833634f7a52e3440be02229e71d4fb (diff)
Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers.
Reviewed-by: ejgallego Reviewed-by: gares
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst5
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
new file mode 100644
index 0000000000..c654ddd69d
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+ Properly report the mismatched magic number of vo files
+ (`#12677 <https://github.com/coq/coq/pull/12677>`_,
+ fixes `#12513 <https://github.com/coq/coq/issues/12513>`_,
+ by Pierre-Marie Pédrot).