Sat, 07 Jul 2007 12:16:16 +0200 markup: emit as control information -- no indent text;
wenzelm [Sat, 07 Jul 2007 12:16:16 +0200] rev 23628
markup: emit as control information -- no indent text;
Sat, 07 Jul 2007 12:16:15 +0200 added property conversions;
wenzelm [Sat, 07 Jul 2007 12:16:15 +0200] rev 23627
added property conversions; tuned;
Sat, 07 Jul 2007 12:16:14 +0200 position: line and name;
wenzelm [Sat, 07 Jul 2007 12:16:14 +0200] rev 23626
position: line and name; tuned operations;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip