Skip to content
Snippets Groups Projects
Commit d77705b9 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Eva] Do not export statistics if not required

parent 9e97fdd6
No related branches found
No related tags found
No related merge requests found
......@@ -178,8 +178,15 @@ let export_as_csv_to_channel out_channel =
in
List.iter (pp_stat fmt) l
let export_as_csv ?filename () =
let default = Parameters.StatisticsFile.get () in
let filename = Option.value ~default filename in
let out_channel = open_out (filename :> string) in
let export_as_csv_to_file filename =
let out_channel = open_out (filename : Filepath.Normalized.t :> string) in
export_as_csv_to_channel out_channel
let export_as_csv ?filename () =
match filename with
| None ->
if not (Parameters.StatisticsFile.is_empty ()) then
let filename = Parameters.StatisticsFile.get () in
export_as_csv_to_file filename
| Some filename ->
export_as_csv_to_file filename
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment