diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 00:32:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-27 16:53:06 +0200 |
| commit | 19f5b6a7d467f75b334e769ebe30cf6459c86855 (patch) | |
| tree | 63c2fe552a85bebae728e13930add7a097159b43 | |
| parent | 64a8f3cbb2fa278ed9d7bf2e5567d4e2b9bfa9dc (diff) | |
[configure] Don't die if the build sandbox doesn't have the stdlib.
Dune calls `./configure` under the build sandbox, which, if the voboot
target has not been executed will contain only the OCaml parts of Coq.
Thus, we make configure not to die if the `plugins` directory is not
present.
This makes Dune usable without calling the `voboot` target.
| -rw-r--r-- | configure.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 1b0c592e46..d010b44e54 100644 --- a/configure.ml +++ b/configure.ml @@ -1239,7 +1239,10 @@ let write_configml f = pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs; pr "\nlet plugins_dirs = [\n"; - let plugins = Sys.readdir "plugins" in + let plugins = + try Sys.readdir "plugins" + with _ -> [||] + in Array.sort compare plugins; Array.iter (fun f -> |