aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2016-11-26 15:26:21 +0100
committerGravatar Hendrik Tews <hendrik@askra.de>2016-11-30 22:48:21 +0100
commit1e506d9da3b05a5ec8c6ec5e91f17cf153cb6dfc (patch)
treebc3b1871073b006d3477dc9bce2886a645ab6ecf
parent1c7dd346c0c94f8b2f5d5f117b8dfd9dfa5a2532 (diff)
fix customize-group coq
-rw-r--r--coq/coq.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 59f3fb04..87641e57 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1786,7 +1786,7 @@ Near here means PT is either inside or just aside of a comment."
(defpacustom search-blacklist coq-search-blacklist-string
"Strings to blacklist in requests to coq environment."
:type 'string
- :get coq-search-blacklist-string
+ ;;:get coq-search-blacklist-string
:setting coq-set-search-blacklist)