https://gcc.gnu.org/bugzilla/show_bug.cgi?id=88607 --- Comment #5 from Jonathan Wakely <redi at gcc dot gnu.org> --- These characters come from copying & pasting text from the PDF of the C++ standard, which uses ligatures. We should just replace the ligature.