# FIXME: Java's `char` are encoded on 16-bits whereas Nit's are on 8-bits.
	fun char_extra(name: JavaString, def_value: Char): Char in "Java" `{
		return (int)self.getCharExtra(name, (char)def_value);
	`}