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 | |
| parent | 8b6f8e5fb85bcd1b3257550270c4c857d4ee7f55 (diff) | |
Implement a Config.ml file which groups all the global options in references
Diffstat (limited to 'compiler/dune')
| -rw-r--r-- | compiler/dune | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/compiler/dune b/compiler/dune index 0d340d59..85f4b75b 100644 --- a/compiler/dune +++ b/compiler/dune @@ -14,6 +14,7 @@ (modules Assumed Collections + Config ConstStrings Contexts Cps |