[PATCH] Make StdVectorPrinter in printers.py compatible with ddd

[Ulrich Drepper]

Frontends will not get predictable results unless they disable pretty
printing and use /r.  If they want some pretty printing to ease the
burden of their own work it is possible to overwrite the
system-provided pretty printers.

Just imagine what happens if a locally defined pretty printer prints
arrays without any commas because it is supposed to be a vector.  Then
the ddd parser won't be able to do anything.

Applying even this one change is a slippery slope because it just
encourages ignoring the problem on the side of the frontends.