Files
mercury/tools
Julien Fischer a0be3c6b79 Update this script in preparation for the 0.12 release.
Estimated hours taken: 0.1
Branches: main, release

tools/run_all_tests_from_cron:
	Update this script in preparation for the 0.12 release.
	Delete references to hosts that no longer exist.
2005-02-01 03:57:00 +00:00
..
2004-02-09 04:56:03 +00:00
2005-01-26 15:56:05 +00:00

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.