aboutsummaryrefslogtreecommitdiffhomepage
path: root/plastic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2006-01-27 17:21:22 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2006-01-27 17:21:22 +0000
commitbb41772fd7842a8b8b27113161fb0fce64c273ed (patch)
treecddbdff05ebc8e4b6515698680e96bcc3369cabf /plastic
parent1b5359dcb5daba5d5e32dc8501a86631f06a8d35 (diff)
Fix from Paul
Diffstat (limited to 'plastic')
-rw-r--r--plastic/plastic.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el
index debbc1a5..33b7179f 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -585,8 +585,8 @@ We assume that module identifiers coincide with file names."
))
(t
(incf i)))) ; else include.
- (setq string (replace-in-string string " *" " "))
- (setq string (replace-in-string string "^ *" ""))
+ (setq string (replace-in-string string " +" " "))
+ (setq string (replace-in-string string "^ +" ""))
(if (string-match "^\\s-*$" string)
(setq string (concat "ECHO comment line" proof-terminal-string))
string))))