Issuing individual INSERTs for each line in the docs works decently when
local, but it slow when loading across The Tubes Of The Internet.
Switching to using COPY takes the load time from the buildfarm animal
from just over 2 minutes to about 6-7 seconds.
It seems the newer tidy in Debian Stretch breaks with the output from
the old docs toolchain, causing indention to happen inside <pre> blocks
which clearly breaks rendering.
Turn it off for thos, but keep it enabled for version 11 and up (at this
point that's just dev), because the output becomes a lot easier to read
when trying to debug things.
This removes the dependency on django from docload, facilitating
incremental upgrades of the infrastructure.
This now requires a new docload.ini file in the tools/docs directory,
with a section "db" and a setting "dsn".
This makes it possible to figure out when the docs were actually
loaded, since developer docs don't carry a version number. This is
actually going to be the docs *load* timestamp, and not build timestamp,
but they should be close enough together that it shouldn't matter.
Fixes#108
