Git: always uses doc/code/.gitignore to ignore the generated code documentation.

.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/

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/