Properly JSON encode null character as \u0000 .
This commit is contained in:
@@ -48,6 +48,7 @@ feature -- Encoder
|
|||||||
if uc.is_character_8 then
|
if uc.is_character_8 then
|
||||||
c := uc.to_character_8
|
c := uc.to_character_8
|
||||||
inspect c
|
inspect c
|
||||||
|
when '%U' then Result.append_string ("\u0000")
|
||||||
when '%"' then Result.append_string ("\%"")
|
when '%"' then Result.append_string ("\%"")
|
||||||
when '\' then Result.append_string ("\\")
|
when '\' then Result.append_string ("\\")
|
||||||
when '%B' then Result.append_string ("\b")
|
when '%B' then Result.append_string ("\b")
|
||||||
|
|||||||
Reference in New Issue
Block a user