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

[Peter Wang]

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.

Index: scripts/Mercury.config.in
===================================================================
RCS file: /home/mercury1/repository/mercury/scripts/Mercury.config.in,v
retrieving revision 1.11
diff -u -r1.11 Mercury.config.in
--- scripts/Mercury.config.in	21 Dec 2005 05:53:04 -0000	1.11
+++ scripts/Mercury.config.in	16 Jan 2006 05:28:59 -0000
@@ -39,6 +39,8 @@
 
 DEFAULT_MERCURY_LINKAGE=@DEFAULT_LINKAGE@
 
+DEFAULT_GRADEFLAGS=--grade "$(MERCURY_DEFAULT_GRADE)"
+
 # The default optimization level should be after
 # all the options that describe the machine configuration.
 DEFAULT_MCFLAGS=\
@@ -47,7 +49,6 @@
 		--cc "$(MERCURY_C_COMPILER)" \
 		--java-compiler "$(MERCURY_JAVA_COMPILER)" \
 		--java-interpreter "$(MERCURY_JAVA_INTERPRETER)" \
-		--grade "$(MERCURY_DEFAULT_GRADE)" \
 		--cflags-for-ansi "@CFLAGS_FOR_ANSI@" \
 		--cflags-for-optimization "@CFLAGS_FOR_OPT@" \
 		--cflags-for-warnings "@CFLAGS_FOR_WARNINGS@" \
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------