diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml index c4c0934db605687aeb685d16abaebc37a0b4e5d6..baf2ca5fd2b43f6e3bb9a1f82b6e8621948e722e 100644 --- a/src/plugins/metrics/metrics_base.ml +++ b/src/plugins/metrics/metrics_base.ml @@ -256,11 +256,11 @@ let get_file_type filename = | "html" | "htm" -> Html | "txt" | "text" -> Text | s -> - Metrics_parameters.fatal + Metrics_parameters.abort "Unknown file extension %s. Cannot produce output.@." s with | No_suffix -> - Metrics_parameters.fatal + Metrics_parameters.abort "File %s has no suffix. Cannot produce output.@." filename module VarinfoByName = struct