Hi Tobias,
*** PING *** The patch is rather simple and almost three weeks old ... Even if it is mostly a no-op patch (as long as FINAL is disabled), I'd like to get it out of my tree.
The patch is fine, as far as I can see.
OK for trunk.
Thomas
