mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-13 12:53:53 +00:00
5acbb7724e
Estimated hours taken: 0.05 A tar file was being misnamed when moved. tools/test_mercury: s/extra/extras
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.