documentation: encode format version into search data filename.

documentation: encode format version into search data filename.

The browser having a stale data (and a stale script) cached is okay-ish
as things still mostly work, but having a stale data with a script
expecting a new version or vice versa is *bad*, so prevent that by
having the script always download file of the exact version it expects.

This is a bit less useful with docs served from local filesystem (as
the filename is encoded in HTML pages rather than in the script), but
there I don't assume the browser is doing much caching so that should be
okay.