[m-rev.] for review: mercury_config --rebase

Julien Fischer juliensf at csse.unimelb.edu.au
Wed Jul 7 14:31:25 AEST 2010


On Wed, 7 Jul 2010, Peter Wang wrote:

> Branches: main, 10.04
>
> Add an option to the `mercury_config' script to make it easier to relocate a
> Mercury installation.
>
> scripts/mercury_config.in:
>        Add the option `--rebase', which acts as if the user passed the options
>        `--input-prefix <dir> --output-prefix <dir>', except that <dir> is
>        automatically guessed from the path to the `mercury_config' script.
>        (--input-prefix is undocumented)
>
>        If `mercury_config' is run without any arguments, and the input
>        directory doesn't exist, suggest the `--rebase' option as the user
>        probably moved the Mercury installation already.
>
>        Don't copy `Mercury.config.bootstrap' to the output directory.
>
>        Copy the regenerated `mdbrc' file to the output directory.
>
>        Set execute permissions on scripts copied to the output bin directory.
>

That's fine.

Julien.
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------



More information about the reviews mailing list