On Tue, Nov 19, 2013 at 1:58 AM, Jan Lehnardt <[email protected]> wrote: > I’m happy to set up a jenkins build that publishes new versions of > the Dash doc set.
Are you saying you'd prefer to not put this in the build system by default, but let it be handled by some Jenkins job? Cheers, Dirkjan
