Am Freitag 04 Oktober 2013, 15:27:54 schrieb stefano franchi:
> I would write:
> resorts|seeERT{ beach resortsERT}
I would even write:
resorts<ERT>|see{</ERT>beach resorts<ERT>}</ERT>
With some font encodings, the "|" will be output as \textbar outside ERT, and
this will break the index.
Jürgen
