From 2a1463131fcf27f33bf2456fc18b2fcdb73044cf Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 27 Aug 2020 08:49:20 +0200
Subject: [PATCH] [Metrics] convert user errors from fatal to abort
---
src/plugins/metrics/metrics_base.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index c4c0934db60..baf2ca5fd2b 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
--
GitLab