From be1183892ce5bfde6ed164e38de7a954fa670646 Mon Sep 17 00:00:00 2001 From: "Jeremy W. Sherman" Date: Sat, 10 Oct 2015 20:34:10 -0400 Subject: [PATCH] Removes :q alias for :abandon As of Idris v0.9.19, :q is no longer accepted by the elab shell. --- docs/reference/elaborator-reflection.rst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/reference/elaborator-reflection.rst b/docs/reference/elaborator-reflection.rst index 17e880791..e52ffeb2a 100644 --- a/docs/reference/elaborator-reflection.rst +++ b/docs/reference/elaborator-reflection.rst @@ -81,8 +81,7 @@ to enter the elaboration shell. The interactive elaboration shell accepts the following commands: -- ``:abandon``, or ``:q`` for short, - quits the elaboration shell, which abandons proving the current lemma. +- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell. - ``:state`` displays the current state of the term being constructed.