On 11/5/18 9:31 AM, Magnus Hagander wrote:
>
> Yes, I think it should be. Also makes it consistent.
>
> With that change as well, lgtm.
Per that change and some brief off-list discussion, this has been pushed.
Andres: thanks again for proposing
Welcome to the new era of doc urls.
Jonathan