aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2009-09-04 15:08:56 +0000
committerDavid Aspinall2009-09-04 15:08:56 +0000
commitbf443eef05580de57fbd5ebfc72b21ab5cf98a8e (patch)
treebb51a431af2d2f81edce31701e20ce262156ee88
parentc1f0849dd42bf5f3bb7fdf44e6773dbdd6e1fc89 (diff)
proof-files-to-buffers, proof-locate-executable: simplify
proof-file-to-buffer: use find-buffer-visiting instead proof-looking-at-syntactic-context: moved here from proof-syntax for compilation
-rw-r--r--generic/pg-user.el1
1 files changed, 0 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 5f0f741e..ef69be7c 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -131,7 +131,6 @@ If inside a comment, just process until the start of the comment."
(forward-char 1)
(proof-assert-until-point)
(goto-char (proof-queue-or-locked-end))
- (message "Gone to %d" (point))
(proof-script-next-command-advance)))
;; NB: "interactive" variant merely for simple docstring.