Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
mlton: Fix environment variable that specifies gmp directory
The environment variable GMP_DIR is changed to WITH_GMP_DIR.
- Loading branch information