aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClément Pit--Claudel2016-02-29 00:06:41 -0500
committerClément Pit--Claudel2016-02-29 00:06:41 -0500
commit84e3373e401fba65e5be74771ff5b443b34361e0 (patch)
treec0bb8d1210fc6a39c837e748a2ebb7acaa762fdf
parent595c2aaf975bdc6afd996806891a5a790684e267 (diff)
Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands)
-rw-r--r--coq/coq.el6
1 files changed, 3 insertions, 3 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 9c255260..40af5aa2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1907,9 +1907,9 @@ 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 ()
(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'
+ (with-no-warnings ;; NB: dynamic scoping of `string' and `action'
+ ;; Don't add the prefix if this is a command sent internally
+ (unless (eq action 'proof-done-invisible)
(setq string (concat coq--time-prefix string))))))
(add-hook 'proof-shell-insert-hook 'coq-preprocessing)