[m-rev.] for review: Put .mh files into Mercury/mhs subdirectory.
Zoltan Somogyi
zoltan.somogyi at runbox.com
Tue Jul 23 16:50:09 AEST 2024
On Tue, 23 Jul 2024 16:03:19 +1000, Julien Fischer <jfischer at opturion.com> wrote:
> I don't really like the idea of users having to be aware of the
> structure of the Mercury
> subdirectory.
This requirement on users is inherent in the use of --use-subdirs.
And the structure is easy enough to figure out, definitely without
grade subdirs, and even with, though the latter is a bit harder.
Basically: it users do not want to have Mercury-generated files
cluttering up the directories containing their .m files, they need to know
where to find them if and when they need them. There is no getting away
from that fact.
Peter: do NOT drop this diff because of this.
Zoltan.
More information about the reviews
mailing list