[m-rev.] Handling pull requests

[Paul Bone]

On Tue, Jan 08, 2013 at 12:21:27PM +1100, Julien Fischer wrote:
> Hi,
> 
> When in doubt, read the documentation.  From the ``Fine Tuning'' section
> of INSTALL:
> 
> #
> #          The option --disable-most-grades reduces the set of installed grades
> #          to a "minimum" level for developers (just the default grade and the
> #          grades corresponding to the `--debug' and `--high-level-code'
> #          options).
> 

Ah,  I think we have a general problem about where to find certain
information.  But it's obvious now that you point it out.

> > This is not what I want configure to do when I only want enough Mercury to
> > bootstrap with, specifically:
> >     .debug is redundant as .decldebug is present.
> >     I don't need debugging at all if I'm bootstrapping.
> >     I only need one of (the best of) the LLC or HLC grades.
> 
> It's the closest thing we currently have that can be used portably.
> 
> > Maybe we should have an option such as --enable-one-grade-only
> 
> I agree.  I prefer --enable-minimal-install as the name though.  (It fits
> in better with the existing --enable-minimal-hlc-trail-install option.)
> 
> If there's general agreement as to what the name should be I'll go ahead
> and implement it.

I agree, this is a good option.

> As and aside: why is INSTALL.git named that, but referred to as INSTALL_GIT
> inside the file?

That's an error.  I suggested the name INSTALL.git to Micheal as it would
match with the README.topic files.

Cheers.

-- 
Paul Bone
http://www.bone.id.au