aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--coq/coq.el6
1 files changed, 4 insertions, 2 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 9e4621aa..9c255260 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1906,9 +1906,11 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
;; Remark: `action' and `string' are known by `proof-shell-insert-hook'
(defun coq-preprocessing ()
- (if coq-time-commands
+ (when coq-time-commands
+ ;; Don't add the prefix if this is a command sent internally
+ (unless (memq 'no-response-display proof-shell-delayed-output-flags)
(with-no-warnings ;; NB: dynamic scoping of `string'
- (setq string (concat coq--time-prefix string)))))
+ (setq string (concat coq--time-prefix string))))))
(add-hook 'proof-shell-insert-hook 'coq-preprocessing)