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