OP#547 remove unwanted things from git

2026-03-29 16:03:32 +02:00
parent 668c4ab2f8
commit 538bd8ef5a
20 changed files with 2 additions and 2937 deletions
--- a/doc/css/common.css
+++ b/doc/css/common.css
@@ -1,8 +0,0 @@
-/* Ensure the search bar doesn't overlap with links */
-.fixed_header {
-  padding-bottom: 25px;
-}
-
-#full_list {
-  padding-top: 15px;
-}