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

Volker Wysk post at volker-wysk.de
Thu Jul 25 14:32:34 AEST 2024


Am Donnerstag, dem 25.07.2024 um 13:28 +1000 schrieb Mark Brown:
> On Wed, Jul 24, 2024 at 8:49 PM Volker Wysk <post at volker-wysk.de> wrote:
> > 
> > Am Mittwoch, dem 24.07.2024 um 12:09 +0200 schrieb Zoltan Somogyi:
> > > 
> > > On Wed, 24 Jul 2024 11:53:00 +0200, Volker Wysk <post at volker-wysk.de> wrote:
> > > Some users of mmc --make *do* need .err files. One reason I mentioned above.
> > > Another is that some people use automatic error-message-processing programs
> > > such as extras/error.
> > 
> > In this case, I would prefer a command line option that triggers the
> > creation (or retention) of the .err files. Or, they also could be placed in
> > the "Mercury" directory, like Peter has suggested. That seems to be the best
> > option to me.
> 
> Error files also need to be readily discoverable by people who aren't
> used to Mercury's build system. Depending on how a project builds,
> error messages to the output stream may quickly scroll out of sight,
> so if the error files are also out of sight then some users may not
> know the error messages even exist. My recollection is that this was
> the reason for not putting .err files in subdirs in the first place.
>
> Personally, I find it pretty annoying to have to hunt around to find
> where a system I'm unfamiliar with stores its errors or logs. I think
> it would be a poor choice of default behaviour.

Different users have different needs. I, for instance, use the Emacs editor,
which reads in the error messages from the compiler and lets you jump to the
errors' places. So I don't need the .err files.

You also can use a shell script to call the compiler. Then, if you don't
need the .err files, you can just delete them after the call...

Bye,
Volker


More information about the users mailing list