Change utf16_native_endian_to_java to consume char16_t

Java chars are fixed to be 16 bits by the standard.

Author: tautschnig

src/util/unicode.cpp

@@ -295,7 +295,7 @@ static void utf16_native_endian_to_java(
 
 /// \param ch: UTF-16 character in architecture-native endianness encoding
 /// \return String in US-ASCII format, with \\uxxxx escapes for other characters
-std::string utf16_native_endian_to_java(const wchar_t ch)
+std::string utf16_native_endian_to_java(const char16_t ch)
 {
   std::ostringstream result;
   const std::locale loc;

src/util/unicode.h

@@ -26,7 +26,7 @@ std::string
 utf32_native_endian_to_utf8(const std::basic_string<unsigned int> &s);
 
 std::wstring utf8_to_utf16_native_endian(const std::string &in);
-std::string utf16_native_endian_to_java(const wchar_t ch);
+std::string utf16_native_endian_to_java(const char16_t ch);
 std::string utf16_native_endian_to_java(const std::wstring &in);
 
 std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide);