diff options
| author | Clément Pit--Claudel | 2016-02-29 00:06:41 -0500 |
|---|---|---|
| committer | Clément Pit--Claudel | 2016-02-29 00:06:41 -0500 |
| commit | 84e3373e401fba65e5be74771ff5b443b34361e0 (patch) | |
| tree | c0bb8d1210fc6a39c837e748a2ebb7acaa762fdf | |
| parent | 595c2aaf975bdc6afd996806891a5a790684e267 (diff) | |
Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands)
| -rw-r--r-- | coq/coq.el | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -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) |
