aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
blob: affb685fcb0b41d70dceefcfc90bf6dce5870407 (plain)
1
2
3
4
5
- **Removed:**
  Confusingly-named and deprecated since 8.11 `-require` option.
  Use the equivalent `-require-import` instead
  (`#12005 <https://github.com/coq/coq/pull/12005>`_,
  by Théo Zimmermann).