§ Fast string concatenation in python3

Apparently, the correct way to do this, in a way that's not O(n^2) is to use the io.StringIO module. The API is:

• x = io.StringIO(): create a string buffer
• x.write(stuff_to_append): append into string buffer with correct realloc()doubling semantics for O(1) amortized per character
• out = x.getvalue(): pull data out of StringIO.
• x.close(): tell the StringIO that we are done and it can free its buffer.

It took quite a bit of trawling the API docs to find this while I was helping a friend speed up some data munging.