Moritz Ulrich <ulrich.moritz <at> googlemail.com> writes: > It's definitely in release_7.8.11 (git commit 6cddf74).
That particular tag is on the wrong side of the merge (on master, not on maint). Again, if you want that particular commit, you need to pull from master, not from maint and not any release published so far. Achim.
