string_append(). These must be artifacts of GvR's rewrite.
Fixed some typos in the leading comment (and re-filled the
paragraphs).
Hope you don't mind, Guido.
Idea and first three implementation rounds due to Barry -- after that
I spent another day on it, hopefully it's enough for now :-)
(Wait for the checkin to Setup.in.)