char
are encoded on 16-bits whereas Nit's are on 8-bits.
# FIXME: Java's `char` are encoded on 16-bits whereas Nit's are on 8-bits.
fun add_extra_array_of_char(name: JavaString, value: Array[Char]): NativeIntent
import Array[Char].length, Array[Char].[] in "Java" `{
char[] java_array = new char[(int)Array_of_Char_length(value)];
for (int i=0; i < java_array.length; ++i)
java_array[i] = (char)Array_of_Char__index(value, i);
return self.putExtra(name, java_array);
`}
lib/android/intent/intent_api10.nit:242,2--251,3