From 54a79c73c2edcfbb4de79460f1acf146243a9394 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 4 Dec 2020 10:36:53 +0100
Subject: [PATCH] remove obsolete entry in .gitignore

---
 .gitignore | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index b458e734ce8..de43450eff5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -193,7 +193,6 @@ Makefile.plugin.generated
 /src/libraries/utils/json.ml
 /src/kernel_internals/runtime/toplevel_boot.ml
 /src/kernel_internals/runtime/fc_config.ml
-/src/kernel_internals/runtime/frama_c_config.ml
 /src/kernel_internals/parsing/logic_lexer.ml
 /src/kernel_internals/parsing/logic_parser.ml
 /src/kernel_internals/parsing/logic_parser.mli
-- 
GitLab