On Oct 24, 2005, at 5:52 PM, Vincent Lefevre wrote: > But then, copy-paste would no longer always work since spaces are > sometimes added at the end of some lines (depending on the terminal > and the context). Please name such systems. We can then know to not use them, and can document in the manual they are broken if we wish.