From 0d8658d7625b65740cbeb2aea476f7218159882e Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 28 Oct 2014 14:05:41 -0700
Subject: [PATCH] feat(emacs/lean-settings): add
 lean-show-proofstate-in-minibuffer option

---
 src/emacs/lean-settings.el | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index b8864c07f..9a6dce42e 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -129,4 +129,9 @@ false (nil)."
   :group 'lean
   :type 'boolean)
 
+(defcustom lean-show-proofstate-in-minibuffer nil
+  "Set this variable to true to show proof state at minibuffer."
+  :group 'lean
+  :type 'boolean)
+
 (provide 'lean-settings)