On 4/5/2016 4:08 PM, Timon Gehr wrote:
Some additional care will need to be taken, e.g.

/+ <backspace> <backspace>

or even simply

/+ comment +/

that should not be a problem.

Reply via email to