aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2019-02-12 15:26:16 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2019-02-12 15:26:16 +0100
commit7a495eb1dc3db6c8dcbb039ef4ccfe2ae6e4bc26 (patch)
tree45bb1fcaedec1a9290fa035cbb40b6f1a01e3fa7
parent737152152f8ebfb752fac0fbcdddc96ad7b18b8a (diff)
Fixes #411.
Stefan's cleanup stumbled on my lack of comments :-(. Some function was supposed to return point found if found.
-rw-r--r--coq/coq-indent.el4
1 files changed, 3 insertions, 1 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index a8d94234..70191cb9 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -522,7 +522,9 @@ 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)
- (forward-comment (point-max)))
+ (when (or (forward-comment (point-max))
+ (looking-at "\\S-"))
+ (point)))
;; (defun same-line (pt pt2)
;; (or (= (line-number-at-pos pt) (line-number-at-pos pt2))))