[m-dev.] How does one set the default compilation grade?

Ralph Becket rafe at cs.mu.OZ.AU
Fri Jul 2 12:10:43 AEST 2004


Fergus Henderson, Friday,  2 July 2004:
> 
> If you want to set the default grade at configure time, you can set
> DEFAULT_GRADE=whatever in the environment before running configure.
> 
> Or alternatively, you can set MERCURY_DEFAULT_GRADE=whatever in
> the environment before running mmc / mmake.

Many thanks.  I've just spent twenty minutes hunting through
configure.ac and aclocal.m4 and the info files for autoconf and I'm
still none the wiser as to how I might add a `--default-grade' option to
configure.  Can someone who groks autoconf help me out?

Ta,
-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------



More information about the developers mailing list