Adding change log for #17392

coq · Mar 17, 2023 · 6309b5e · 6309b5e
1 parent 2463c7b
commit 6309b5e
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/doc/changelog/09-cli-tools/17392-master+add-output-directory.rst b/doc/changelog/09-cli-tools/17392-master+add-output-directory.rst
@@ -0,0 +1,7 @@
+- **Added:**
+  Command line option :n:`-output-directory dir` to set default output directory
+  for extraction, :cmd:`Redirect` and :cmd:`Print Universes`
+  (`#17392 <https://github.com/coq/coq/pull/17392>`_,
+  fixes `#8649 <https://github.com/coq/coq/issues/8649>`_
+  and `#9148 <https://github.com/coq/coq/issues/9148>`_,
+  by Hugo Herbelin).