Redirect build products to distinct file-tree

[mn200]

In some circumstances (e.g., HOL is installed in read-only filesystem after an initial build), it would be useful to be able to build script files (from examples, for example) without dropping products in the same directory / area. The existing HOLFileSys module already lets us lie about exactly where things like *Theory.dat live; perhaps this facility could be used to redirect outputs to somewhere else entirely.

Thanks to @binghe for discussion leading to this idea.