diff options
| author | Théo Zimmermann | 2020-02-18 19:47:40 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-18 19:47:40 +0100 |
| commit | f208f65ee8ddb40c9195b5c06475eabffeae0401 (patch) | |
| tree | 3f6e5d9f1c1bffe3e4187131f87d3187a8d9ebe5 /tools | |
| parent | af3fd09e2f0cc2eac2bc8802a6818baf0c184563 (diff) | |
| parent | 83052eff43d3eeff96462286b69249ef868bf5f0 (diff) | |
Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.
Reviewed-by: Zimmi48
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_dune.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index f62947ec67..96fb9710c7 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -213,7 +213,7 @@ let record_dune d ff = if Sys.file_exists sd && Sys.is_directory sd then let out = open_out (bpath [sd;"dune"]) in let fmt = formatter_of_out_channel out in - if List.nth d 0 = "plugins" || List.nth d 0 = "user-contrib" then + if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then fprintf fmt "(include plugin_base.dune)@\n"; out_install fmt d ff; List.iter (pp_dep d fmt) ff; @@ -285,8 +285,11 @@ let exec_ifile f = begin try let ic = open_in in_file in (try f ic - with _ -> eprintf "Error: exec_ifile@\n%!"; close_in ic) - with _ -> eprintf "Error: cannot open input file %s@\n%!" in_file + with exn -> + eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn); + close_in ic) + with _ -> + eprintf "Error: cannot open input file %s@\n%!" in_file end | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 |