Yeah, I planned to do that, but after Tuesday (no time ATM).  Shall I change the existing commit in order to add the doc prefix, too?  As far as I can see, that would probably kill this discussion when (force-)pushed, right?