On Tue 11 Dec 2018 at 14:11, Michael Albinus <michael.albinus@gmx.de> wrote:

> Then you shouldn't mention it.

Ugh, missed that. Sorry.

> Furthermore, pls write "TREE" as "@var{tree}".

Thanks, changed. Updated patch attached.

Alex