From 8ac8f5aa327ca8de66e90bb33d1950d9a4749177 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 3 Apr 2020 10:27:15 +0200
Subject: Update
 doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst

Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>---
 doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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).
-- 
cgit v1.2.3