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.