mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-16 14:25:56 +00:00
tools/build_srcdist:
Save the git commit id a srcdist is based upon in a file
within that srcdist.
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.