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

[Volker Wysk]

Am Mittwoch, dem 24.07.2024 um 18:28 +1000 schrieb Peter Wang:
> On Wed, 24 Jul 2024 09:13:49 +0200 Volker Wysk <post at volker-wysk.de> wrote:
> > Am Mittwoch, dem 24.07.2024 um 16:29 +1000 schrieb 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.
> > 
> > I never needed to open a .err file. I'm using "--make" and the compiler
> > outputs all error messages...
> 
> Yes, I would prefer to put .err files in a subdir whenever --use-subdirs
> or --use-grade-subdirs is in effect (that includes mmc --make).
> 
> Users using mmake *do* need to open .err files, but mmake doesn't use
> subdirs by default, so maybe that is fine.

Yes, it has to be good for something, or it wouldn't be this way. It's just
that users of "--make" don't need those .err files.

Cheers,
Volker