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().

diff --git a/src/CutAndPaste.cpp b/src/CutAndPaste.cpp
index 3cc40022bc89957a8d8213e1b345887f683003b7..582875aa3b9cba9394db1f4eb23d407ed65a7869 100644 (file)
--- a/src/CutAndPaste.cpp
+++ b/src/CutAndPaste.cpp
@@ -172,7 +172,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;