11 Nov
2011
11 Nov
'11
8:34 a.m.
Hi Hans, quite often I wish we could have a kind of in line comment: Something like ¿this is my comment¡ this. I assume it is not trivial due to catcode issues, to say the least. But nevertheless, as it is getting close to christmas, I just wanted to mention this idea here. Thanks, Steffen