From edf716fb256dd5dc7210b26a786ff793a96175e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 15 Sep 2021 15:31:03 +0200
Subject: [PATCH] [sparecode] Removes an unused declaration.

---
 src/plugins/sparecode/globs.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index bdbc159416c..2beb56b0239 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -26,7 +26,6 @@ open Cil
 let dkey = Sparecode_params.register_category "globs"
 
 let debug format = Sparecode_params.debug ~dkey ~level:2 format
-let debug' format = Sparecode_params.debug ~dkey ~level:3 format
 
 let used_variables = Hashtbl.create 257
 let var_init = Hashtbl.create 257
-- 
GitLab