Gilles Peskine 49af2d3a4f Support non-ASCII characters in headers
Filter out non-ASCII characters in automatically processed headers.

Do this in a way that minimizes the code change: keep manipulating
strings, but strip off non-ASCII characters when reading lines, which
should only remove characters in comments that we don't parse anyway.
2019-12-11 11:03:07 +01:00
..
2019-11-26 19:12:35 +01:00
2016-01-12 14:48:03 +00:00
2019-11-13 14:33:34 +00:00
2019-02-27 11:03:25 +01:00