diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2006-01-27 17:21:22 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2006-01-27 17:21:22 +0000 |
commit | bb41772fd7842a8b8b27113161fb0fce64c273ed (patch) | |
tree | cddbdff05ebc8e4b6515698680e96bcc3369cabf /plastic | |
parent | 1b5359dcb5daba5d5e32dc8501a86631f06a8d35 (diff) |
Fix from Paul
Diffstat (limited to 'plastic')
-rw-r--r-- | plastic/plastic.el | 4 |
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)))) |