Hello all,
Font and character encodings are tricky, and there are *many* copy and paste issues when trying to copy from PDF files.
In particular from files that are well generated. In my experience copy&paste is flawed in 90% of the PDF files.
Just today I had a similar issue with the regular dash: - of which at least 4 different versions exist in good fonts.
Consider ligatures. If you want a good typography, you want ligatures, but this can break e.g. email adresses etc.
Furthermore, there are diacritics, which are often represented internally as composed characters, but they may or may not be encoded this way in your font.
Oh, and don't forget about quotation marks!
There is little you can do to ensure perfect copy&paste from PDF across different viewers.
And it clearly is not worth the effort. It's likely not an error in the source.
Tl;dr: never assume you can copy&paste from a PDF file.
In particular not from a file that looks good...
If you want to copy some code fragment, copy it from the source files, not a PDF.
(Don't blame me, I didn't invent typography or the PDF file format which is designed for visuals but not for copy&paste.)
Regards,