mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-15 09:23:44 +00:00
tools/import_srcdist:
Check with "git status" that all files in the workspace have been
added, not ignored.
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.