[m-rev.] for post-commit review: inline build_module_with_options

[Julien Fischer]

On Thu, 19 Aug 2021, Zoltan Somogyi wrote:

> Inline all calls to build_module_with_options.
> 
> compiler/make.build.m:
>     Delete build_module_with_options after inlining it at all its call sites.
>     The resulting code is easier to understand, and should be easier
>     to modify.
>
>     Transfer its documentation, suitably modified, to its replacement.

That's fine.

Julien.