[m-users.] [mercury-users] .mh files

[Peter Wang]

On Wed, 24 Jul 2024 06:54:25 +0200 Volker Wysk <post at volker-wysk.de> wrote:
> Am Mittwoch, dem 24.07.2024 um 14:43 +1000 schrieb Peter Wang:
> > 
> > rotd-2024-07-23 now places .mh files in a Mercury/mhs subdirectory.
> 
> What about the .err files?

No change yet.

I think we would have to put it behind an option to avoid disrupting
people's workflows, say:

--error-files-in-subdir
    When --use-subdirs [or --use-grade-subdirs?] is in effect,
    place .err files in a Mercury/errs subdirectory instead of the
    current directory.

Since error messages can depend on grade, it's arguable that if
--use-grade-subdirs is in effect then .err files should be placed in a
grade-specific directory,
e.g. Mercury/hlc.gc/x86_64-pc-linux-gnu/Mercury/errs,
even if that would be less convenient to open.

Peter