Re: Fixes to auxiliar/doc-section.sh

[Trevor Daniels]

Hi Phil, you wrote Saturday, March 10, 2012 10:16 AM

> Once you have a successful make doc, you might be surprised how little 
> time it takes to remake to check changes now.  On my admittedly quick 
> machine, make -j9 CPU_COUNT=9 LANGS='' doc takes about 5 seconds.

It's certainly a lot better than it was and it would be usable even on my
laptop running Ubuntu in 800Mb and 1 processor under VirtualBox.

I find make LANGS='' doc takes 4-5 minutes after a trivial change to
a single file, which I agree is quite workable now.

With the same change the script takes around 2 minutes, but in addition
checks all the cross-references and opens up the section's html in a
browser automatically.  Also there is an option to retain all the snippets
between invocations, which reduces the time to less than 30 seconds -
very useful if you know the changes are all in straight text.

Trevor