diff options
| author | Philipp G. Haselwarter | 2020-06-18 15:46:20 +0100 |
|---|---|---|
| committer | Philipp G. Haselwarter | 2020-06-18 15:46:20 +0100 |
| commit | 543c2807aec1182b9a006abd233548f3459a02c6 (patch) | |
| tree | 574f7b350168e03875ddc83856a4e36402c6f7f5 | |
| parent | 0f0bb2c00fb7b20fd187cb92d4d2c3f84c4c5987 (diff) | |
Use `proof-shell-string-match-safe` to avoid failing on `nil` regexp
Fixes a regression introduced in 22681a3caf2c8f45700585ea74dffbf48bb2ac19.
In particular, the Coq module seems to be the only one currently setting
`proof-show-proof-diffs-regexp`, causing an error for EasyCrypt.
| -rw-r--r-- | generic/proof-shell.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 78b36ee7..af9b50e0 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1197,7 +1197,9 @@ contains only invisible elements for Prooftree synchronization." (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) proof-action-list) ;; If the last command in proof-action-list is a "Show Proof" form then return t - (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) + (when last-command + (proof-shell-string-match-safe + proof-show-proof-diffs-regexp last-command))))))))) (defun proof-shell-insert-loopback-cmd (cmd) |