<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Sep 17, 2013 at 10:15 AM, Peter Wang <span dir="ltr"><<a href="mailto:novalazy@gmail.com" target="_blank">novalazy@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Fri, 6 Sep 2013 18:47:08 +1000 (EST), Julien Fischer <<a href="mailto:jfischer@opturion.com">jfischer@opturion.com</a>> wrote:<br>

> @@ -2047,6 +2056,9 @@ detect_libgrades(Globals, MaybeConfigMerStdLibDir, GradeOpts, !IO) :-<br>
>       globals.lookup_bool_option(Globals, detect_libgrades, Detect),<br>
>       (<br>
>           Detect = yes,<br>
> +        globals.lookup_bool_option(Globals, verbose, Verbose),<br>
> +        maybe_write_string(Verbose, "% Detecting library grades ...\n", !IO),<br>
> +        globals.lookup_bool_option(Globals, very_verbose, VeryVerbose),<br>
>           % NOTE: a standard library directory specified on the command line<br>
>           % overrides one set using the MERCURY_STDLIB_DIR variable.<br>
>           ( if<br>
<br>
</div>mmc -v:<br>
<div class="im"><br>
    % Detecting library grades ...<br>
</div>    % done.<br>
    Mercury Compiler, version rotd-2013-09-10, configured for i686-pc-linux-gnu<br>
    Copyright (C) 1993-2013 The University of Melbourne<br>
    Usage: mmc [<options>] <arguments><br>
    Use `mmc --help' for more information.<br>
<br>
mmc -V:<br>
<div class="im"><br>
    % Detecting library grades ...<br>
</div>    % Detected library grade: hlc.gc<br>
    % Detected library grade: asm_fast.gc<br>
    % Detected library grade: hlc.gc.pregen<br>
    % done.<br>
    Mercury Compiler, version rotd-2013-09-10, configured for i686-pc-linux-gnu<br>
    Copyright (C) 1993-2013 The University of Melbourne<br>
    Usage: mmc [<options>] <arguments><br>
    Use `mmc --help' for more information.<br></blockquote><div><br></div><div style>Hmmm.  I guess we will have to print the set of detected library grades out later.</div><div style><br></div><div style>Cheers,</div>
<div style>Julien.</div><div><br></div><div><br></div><div><br></div><div> </div></div><br></div></div>