From 59fad4b75747b0f8b5cd1d386bbaf8be769d0c9d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 28 Mar 2019 09:32:28 +0100
Subject: [PATCH] [Distribution] remove duplicates

---
 headers/header_spec.txt | 2 --
 1 file changed, 2 deletions(-)

diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 8538850d61e..2f826961dbc 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -664,8 +664,6 @@ src/libraries/utils/pretty_utils.ml: CEA_LGPL
 src/libraries/utils/pretty_utils.mli: CEA_LGPL
 src/libraries/utils/qstack.ml: CEA_LGPL
 src/libraries/utils/qstack.mli: CEA_LGPL
-src/libraries/utils/sanitizer.ml: CEA_LGPL
-src/libraries/utils/sanitizer.mli: CEA_LGPL
 src/libraries/utils/rangemap.ml: OCAML_STDLIB
 src/libraries/utils/rangemap.mli: OCAML_STDLIB
 src/libraries/utils/rgmap.ml: CEA_LGPL
-- 
GitLab