From c301a51e127e0ba812e18785deccd80d2a547d18 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 Jul 2022 08:31:17 +0200
Subject: [PATCH] [wp] lint Stats
---
src/plugins/wp/Stats.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index 475989e0daf..1e74de3f585 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -300,10 +300,10 @@ let pp_stats ~shell ~cache fmt s =
if s.trivial = total then
Format.fprintf fmt " (Trivial)"
else
- if updating || s.cached = cacheable then
- Format.fprintf fmt " (Cached)"
- else
- Format.fprintf fmt " (Cached %d/%d)" s.cached cacheable
+ if updating || s.cached = cacheable then
+ Format.fprintf fmt " (Cached)"
+ else
+ Format.fprintf fmt " (Cached %d/%d)" s.cached cacheable
let pretty = pp_stats ~shell:false ~cache:NoCache
--
GitLab