diff options
| author | Théo Zimmermann | 2020-04-03 10:27:15 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-03 10:27:15 +0200 |
| commit | 8ac8f5aa327ca8de66e90bb33d1950d9a4749177 (patch) | |
| tree | 1fa9917ed1d1a8ea74b8cf000155426190523b89 | |
| parent | e3e1133fe5685213460a6cc3f761283815223e3d (diff) | |
Update doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
| -rw-r--r-- | doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 2 |
1 files changed, 1 insertions, 1 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 index e38f2f337a..affb685fcb 100644 --- a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst +++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst @@ -1,5 +1,5 @@ - **Removed:** Confusingly-named and deprecated since 8.11 `-require` option. - Use `-require-import` instead + Use the equivalent `-require-import` instead (`#12005 <https://github.com/coq/coq/pull/12005>`_, by Théo Zimmermann). |