Jürgen Spitzmüller wrote:
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.
OK, sorry, I see where I got confused. In replace(), one has to do it
that way. But in strings passed to re, you do need the double backslash.
Thus, it has to be:
m = re.match(r'(.*)\\InsetSpace (.*)', document.body[i])
not:
m = re.match(r'(.*)\InsetSpace (.*)', document.body[i])
I take it the reason is that re itself has its own way of understanding "\".
rh
