aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-22 14:31:17 +0000
committerGitHub2021-02-22 14:31:17 +0000
commit64f12dec42adeaeb06266ab8aadd56a9f544b823 (patch)
tree3c05ac574d2190317b1105163691be2573da18d1
parent0ee4a8903597527d3872471c87064d9645c9a91b (diff)
parent2c1e2cda670e720156a32a16e7999548cd41cc94 (diff)
Merge PR #13878: [RM] Changelog for 8.13.1
Reviewed-by: Zimmi48
-rw-r--r--doc/changelog/01-kernel/13867-changelog-for-13867.rst5
-rw-r--r--doc/sphinx/changes.rst21
2 files changed, 21 insertions, 5 deletions
diff --git a/doc/changelog/01-kernel/13867-changelog-for-13867.rst b/doc/changelog/01-kernel/13867-changelog-for-13867.rst
deleted file mode 100644
index 37e44b41c7..0000000000
--- a/doc/changelog/01-kernel/13867-changelog-for-13867.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
- Fix arities of VM opcodes for some floating-point operations
- that could cause memory corruption
- (`#13867 <https://github.com/coq/coq/pull/13867>`_,
- by Guillaume Melquiond).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 4769636ae8..ea099eb52e 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -701,6 +701,27 @@ Commands and options
(`#13556 <https://github.com/coq/coq/pull/13556>`_,
by Simon Friis Vindum).
+Changes in 8.13.1
+~~~~~~~~~~~~~~~~~
+
+Kernel
+^^^^^^
+
+- **Fixed:**
+ Fix arities of VM opcodes for some floating-point operations
+ that could cause memory corruption
+ (`#13867 <https://github.com/coq/coq/pull/13867>`_,
+ by Guillaume Melquiond).
+
+CoqIDE
+^^^^^^
+
+- **Added:**
+ Option ``-v`` and ``--version`` to CoqIDE
+ (`#13870 <https://github.com/coq/coq/pull/13870>`_,
+ by Guillaume Melquiond).
+
+
Version 8.12
------------