aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-indent.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2014-12-30 14:07:21 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2014-12-30 14:07:21 +0000
commit22d7dccdd23603d07975799a159623223cb31095 (patch)
treee2c0f5b16de90534b7d2aba29a6668e29ef6b485 /coq/coq-indent.el
parentb75bf02626b639bad8fe28796b7ee9163fd54323 (diff)
removed debug message.
Diffstat (limited to 'coq/coq-indent.el')
-rw-r--r--coq/coq-indent.el1
1 files changed, 0 insertions, 1 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 352931c0..da73f808 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -327,7 +327,6 @@ command end regexp."
(not (coq-empty-command-p)))
nil)
(and
- (message "ICI")
(goto-char foundend)
(proof-buffer-syntactic-context))))
;; go back as far as possible before the start of the current