aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2019-02-12 15:33:53 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2019-02-12 15:33:53 +0100
commit8f90ac961c22099a615c03ed07576aaef820e06d (patch)
tree013b87c2867e0c23a5ffd12ae59afad89fc21ff9
parent7a495eb1dc3db6c8dcbb039ef4ccfe2ae6e4bc26 (diff)
Simpler fix for #411.
-rw-r--r--coq/coq-indent.el5
1 files changed, 2 insertions, 3 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 70191cb9..9ca75457 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -522,9 +522,8 @@ the (point-min) if there is no previous command."
"Move to the start of command at point.
The point is put exactly before first non comment letter of the command."
(coq-find-current-start)
- (when (or (forward-comment (point-max))
- (looking-at "\\S-"))
- (point)))
+ (forward-comment (point-max))
+ (point))
;; (defun same-line (pt pt2)
;; (or (= (line-number-at-pos pt) (line-number-at-pos pt2))))