[m-rev.] for review: move default --grade option into GRADEFLAGS

[Julien Fischer]

On Tue, 17 Jan 2006, Peter Wang wrote:

> Estimated hours taken: 1
> Branches: main
>
> scripts/Mercury.config.in:
> 	Move the default `--grade' option from DEFAULT_MCFLAGS to
> 	DEFAULT_GRADEFLAGS.  `mmc --make' generates command-lines with
> 	MCFLAGS options after GRADEFLAGS options, so GRADEFLAGS set by
> 	the user were being overridden by the default `--grade' option
> 	in MCFLAGS.
>
That's fine.

Cheers,
Julien.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------