diff options
| author | Maxime Dénès | 2017-12-27 10:19:21 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:21 +0100 |
| commit | 4969f9425cb0d5cd5bd735110886a0cbd2641588 (patch) | |
| tree | 6c05276df78dd476642ab5db8437e8730d19eb56 /configure.ml | |
| parent | 3921ff2e2c189063ec46f54cbb247570b6c59b2c (diff) | |
| parent | 5ffa147bd2fe548df3ac9053fe497d0871a5f6df (diff) | |
Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 06aa5e7666..0698d93e26 100644 --- a/configure.ml +++ b/configure.ml @@ -1143,7 +1143,7 @@ let write_configml f = core_src_dirs in pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs; - pr "\nlet api_dirs = [\"API\"; \"lib\"]\n"; + pr "\nlet api_dirs = [\"API\"; \"clib\"; \"lib\"]\n"; pr "\nlet plugins_dirs = [\n"; let plugins = Sys.readdir "plugins" in |