diff options
| -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 -> |