Correctly output a single char_type

On platforms where char_type is typedef'd to an integral type
rather than to wchar_t, when using the insertion operator <<
a single char_type is output as the number corresponding to the
code point of the character rather than as the character itself.
In this case, one has to use put().

(cherry picked from commit 144f06a00c58619557fb431877041fd9e4297a0f)

diff --git a/src/CutAndPaste.cpp b/src/CutAndPaste.cpp
index e7f38b35c880e2a73edf1d2f0a66a56bfe19ab27..f611d59395b8b9681b5a0d20c89435f1c684c52e 100644 (file)
--- a/src/CutAndPaste.cpp
+++ b/src/CutAndPaste.cpp
@@ -171,7 +171,7 @@ pasteSelectionHelper(DocIterator const & cur, ParagraphList const & parlist,
                                char_type const c = insertion[i].getChar(j);
                                if (!e->encodable(c)) {
                                        // do not track deletion
-                                       res << c;
+                                       res.put(c);
                                        insertion[i].eraseChar(j, false);
                                        --end;
                                        --j;