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

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;