diff options
| author | Son Ho | 2022-11-09 19:06:03 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-10 11:35:30 +0100 |
| commit | 98ecc4763beb6c6213b26f4ddeb4d7850f8a7c08 (patch) | |
| tree | d125e829bb2e3343eccde56fb7b20614ef732d87 /compiler/dune-project | |
| parent | 8b6f8e5fb85bcd1b3257550270c4c857d4ee7f55 (diff) | |
Implement a Config.ml file which groups all the global options in references
Diffstat (limited to 'compiler/dune-project')
0 files changed, 0 insertions, 0 deletions