-
Herbert Valerio Riedel authored
Turns out that special care needs to be taken when escaping `|`s in `\index{}`. See also http://tex.stackexchange.com/questions/176931/how-to-escape-character-in-index
69337bce
Turns out that special care needs to be taken when escaping `|`s in `\index{}`. See also http://tex.stackexchange.com/questions/176931/how-to-escape-character-in-index