Fix part of #3398: pretty-printing always goes via the I/O library encoding