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

Volker Wysk post at volker-wysk.de
Wed Jul 24 14:54:25 AEST 2024


Am Mittwoch, dem 24.07.2024 um 14:43 +1000 schrieb Peter Wang:
> On Thu, 18 Jul 2024 11:14:33 +1000 Peter Wang <novalazy at gmail.com> wrote:
> > On Wed, 17 Jul 2024 15:43:32 +0200 Anders Lundstedt <mercury-users at anderslundstedt.se> wrote:
> > > On Fri Aug 15 13:25:46 AEST 2003 Fergus Henderson wrote:
> > > > > On 13-Aug-2003, Michael Day <mikeday at yeslogic.com> wrote:
> > > > > 
> > > > > Is there a way to make the .mh files live in the Mercury directory instead
> > > > > of cluttering up the current directory?
> > > > 
> > > > Currently no.
> > > 
> > > Is this possible now?
> > 
> > Still no.
> > 
> > I'm not seeing a reason why .mh files cannot be placed in Mercury/mhs.
> 
> rotd-2024-07-23 now places .mh files in a Mercury/mhs subdirectory.

What about the .err files?

Volker


More information about the users mailing list