mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-16 09:53:36 +00:00
The code it deleted turned out to be needed; the need for it was just undocumented. A future diff will supply that documentation.
The code it deleted turned out to be needed; the need for it was just undocumented. A future diff will supply that documentation.