diff options
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 2 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 5f4add47a..98c485dba 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -351,7 +351,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids if computeinnertypes then try Acic.CicHash.find terms_to_types tt -with _ -> +with e when Errors.noncritical e -> (*CSC: Warning: it really happens, for example in Ring_theory!!! *) Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false else diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 4d9541ebc..a34d4a682 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -81,7 +81,7 @@ let rec join_dirs cwd = | he::tail -> (try Unix.mkdir cwd 0o775 - with _ -> () (* Let's ignore the errors on mkdir *) + with e when Errors.noncritical e -> () (* ignore the errors on mkdir *) ) ; let newcwd = cwd ^ "/" ^ he in join_dirs newcwd tail |