http://gcc.gnu.org/bugzilla/show_bug.cgi?id=52539
--- Comment #11 from Andreas Schwab <[email protected]> --- Mixing push_char and push_char4 can't be right.
http://gcc.gnu.org/bugzilla/show_bug.cgi?id=52539
--- Comment #11 from Andreas Schwab <[email protected]> --- Mixing push_char and push_char4 can't be right.