diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-06-06 11:43:15 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-06-06 11:43:15 +0200 |
| commit | 9170b7ea371fdf020411e787df937b278a394e57 (patch) | |
| tree | 8d1416a33725082fded3b16cc875b2d5c6451b92 /generic | |
| parent | b392b77a1e247905fbc0a1cce1a2b494878836b8 (diff) | |
Fixing bug #187 by removing trailing spaces from prog name.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 7d3fe5b9..6f3180fe 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -284,6 +284,13 @@ In this case `proof-shell-filter' must be called again after it finished.") (setq pg-response-special-display-regexp (proof-regexp-alt goals resp trace thms)))) +(defun proof-strip-whitespace-at-end (string) + "Return STRING stripped of all trailing whitespace." + (while (string-match "[\r\n\t ]+$" string) + (setq string (replace-match "" t t string))) + string) + + (defun proof-shell-start () "Initialise a shell-like buffer for a proof assistant. Does nothing if proof assistant is already running. @@ -306,8 +313,9 @@ process command." (if proof-prog-name-ask ;; if this option is set, an absolute file name is better to show if possible (let ((prog-name (locate-file proof-prog-name exec-path exec-suffixes 1))) - (setq proof-prog-name (read-shell-command "Run process: " - prog-name)))) + (setq proof-prog-name (proof-strip-whitespace-at-end + (read-shell-command "Run process: " + prog-name))))) (let ((proc (downcase proof-assistant))) |