From ea7f5bade7ce1ed74f95516df26df769b30c8d72 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 Jul 2022 13:31:40 +0200
Subject: [PATCH] [wp] json report is always pretty
---
src/plugins/wp/register.ml | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 82763ef243f..2a2f331d902 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -284,9 +284,7 @@ let do_report_json () =
let js = stats_to_json g s in
js :: json
) !session [] in
- let pretty =
- Wp_parameters.verbose_atleast 2 || Wp_parameters.debug_atleast 1 in
- Json.save_file ~pretty file (`List json)
+ Json.save_file file (`List json)
(* -------------------------------------------------------------------------- *)
(* --- Prover Results --- *)
--
GitLab