From 6f05a46e08fdb8de2319c36f07a737b1acebfe31 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 May 2019 17:23:37 +0200
Subject: Updated changelog.

---
 doc/changelog/08-tools/10245-require-command-line.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/08-tools/10245-require-command-line.rst

(limited to 'doc')

diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst
new file mode 100644
index 0000000000..54417077f5
--- /dev/null
+++ b/doc/changelog/08-tools/10245-require-command-line.rst
@@ -0,0 +1,6 @@
+- Add command line options `-require-import`, `-require-export`,
+  `-require-import-from` and `-require-export-from`, as well as their
+  shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate
+  confusing command line option `-require`
+  (`#10245 <https://github.com/coq/coq/pull/10245>`_
+  by Hugo Herbelin, review by Emilio Gallego).
-- 
cgit v1.2.3