aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml/xmlcommand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
-rw-r--r--contrib/xml/xmlcommand.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 1aabd4348..82d7c19e5 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -691,11 +691,11 @@ let _ =
Buffer.output_buffer ch theory_buffer ;
close_out ch
end ;
- Util.option_iter
+ Option.iter
(fun fn ->
let coqdoc = Coq_config.bindir^"/coqdoc" in
let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
- let dir = Util.out_some xml_library_root in
+ let dir = Option.get xml_library_root in
let command cmd =
if Sys.command cmd <> 0 then
Util.anomaly ("Error executing \"" ^ cmd ^ "\"")