rgheck wrote:
> Fix a bunch of backslashes.
>
> If this is wrong, someone revert it. But I think it must be right.
> - line = line.replace(r'\backslash', r'\textbackslash{}')
[...]
> + line = line.replace(r'\\backslash', r'\\textbackslash{}')I think the r prefix marks the string as a raw string where special characters (such as the backslash) don't need to (and in fact must not) be escaped: http://www.python.org/doc/current/ref/strings.html So I think this fix is wrong. Jürgen
