mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-15 01:13:30 +00:00
Mmake.common.in:
RELEASE_NOTES:
configure.ac:
scripts/mgnuc.in:
tools/bootcheck:
tools/configure_cross:
tools/copy_mercury_binaries:
Conform to the recent change that moved most of the README files into the
Documentation directory.
This directory, mercury/tools, contains scripts that are not intended for use by users. The scripts here are used by the Mercury developers for maintaining the Mercury compiler.