aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
authorVincent Laporte2019-03-25 16:05:49 +0000
committerVincent Laporte2019-03-25 16:05:49 +0000
commit1fa29f0558351634ad5b30876fb089bd22bf28ad (patch)
tree7bfd767e4af955578f79e58d7636bf2b44bb6d14 /doc/sphinx/proof-engine
parentce97ef5375e1596cd7b2510cf576f2961329f523 (diff)
[Vernacular] Deprecate the “Show Script” command
Fixes #8320
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 07215a0c7e..16b158c397 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -544,6 +544,10 @@ Requesting information
``<Your Tactic Text here>``.
+ .. deprecated:: 8.10
+
+ Please use a text editor.
+
.. cmdv:: Show Proof
:name: Show Proof