[m-dev.] Re: trivial diff: scripts/parse_grade_options.sh-subr bug fix

[Thomas Charles CONWAY]

Fergus Henderson, you write:
> Well, we already have a way to add a grade element: just use the
> relevant options (e.g. `--use-trail'; for compound grade elements
> such as `fast' you may need to use several options, e.g.
> `--use-gcc-nonlocal-gotos --use-gcc-global-registers --no-use-asm-labels').
> So since there's already a way of adding grade elements, and also for
> backwards compatibility, I think `--grade' should override the grade
> completely.

I guess you can then do stuff like the following:
	--grade fast --use-trail
I expect the common need is to set a bunch with a --grade option
then tweak them with separate options.

I'll implement --grade so that it resets the grade dependent options.

Thomas
-- 
Thomas Conway <conway at cs.mu.oz.au>
Nail here [] for new monitor.  )O+