diff options
| author | Théo Zimmermann | 2020-04-02 15:59:53 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-02 22:14:27 +0200 |
| commit | cb1e693d84013b56c9a8e6154e101245c950f85f (patch) | |
| tree | 669610613946175f026e0d451076f2440aa79c25 | |
| parent | 0c1382bd0a9c41b559a912695e2154b758de7b18 (diff) | |
Add changelog entry for #12005.
| -rw-r--r-- | doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst new file mode 100644 index 0000000000..e38f2f337a --- /dev/null +++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst @@ -0,0 +1,5 @@ +- **Removed:** + Confusingly-named and deprecated since 8.11 `-require` option. + Use `-require-import` instead + (`#12005 <https://github.com/coq/coq/pull/12005>`_, + by Théo Zimmermann). |