From 693ed00edc7b6756b99d1e294460652e704b45e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 15 Sep 2021 10:16:07 +0200
Subject: [PATCH] Git: always uses doc/code/.gitignore to ignore the generated
 code documentation.

---
 .gitignore          | 5 -----
 doc/code/.gitignore | 2 ++
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/.gitignore b/.gitignore
index a99e667dc23..6739522d9eb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -116,11 +116,6 @@ autom4te.cache
 /doc/code/print_api/dynamic_plugins.mli
 /doc/code/print_api/_build/
 
-/doc/code/builtin
-/doc/code/studia
-/doc/code/qed
-/doc/code/wp
-
 /doc/developer/tutorial/viewcfg/src/META.frama-c-viewcfg
 /doc/developer/tutorial/viewcfg/src/Makefile
 /doc/developer/tutorial/viewcfg/src/gui/
diff --git a/doc/code/.gitignore b/doc/code/.gitignore
index 1d73c356b60..94c6462e29b 100644
--- a/doc/code/.gitignore
+++ b/doc/code/.gitignore
@@ -25,6 +25,7 @@
 /pdg/
 /postdominators/
 /print_api/
+/qed/
 /reduc/
 /report/
 /rte/
@@ -32,6 +33,7 @@
 /security_slicing/
 /slicing/
 /sparecode/
+/studia/
 /users/
 /value/
 /variadic/
-- 
GitLab