In 2006 we imported this from www.gnu.org to align our appearance
with the one there. Alas, that site kept evolving (and inconsistently
so), and in fact removed this style, and I'll be trying to clean this
up now.
This is the first step, removing a number of unused styles.
Applied.
Gerald
Index: gnu.css
===================================================================
RCS file: /cvs/gcc/wwwdocs/htdocs/gnu.css,v
retrieving revision 1.3
diff -u -r1.3 gnu.css
--- gnu.css 21 Sep 2006 14:17:36 -0000 1.3
+++ gnu.css 3 Apr 2011 13:17:15 -0000
@@ -1,7 +1,7 @@
/*
gnu.css -- css stylesheet used on www.gnu.org
-Copyright (C) 2006 Free Software Foundation
+Copyright (C) 2006, 2011 Free Software Foundation
Permission is hereby granted, free of charge, to any person
obtaining a copy of this software and associated documentation
@@ -85,13 +85,6 @@
font-size: smaller;
}
-.translations {
- background-color: transparent;
- color: black;
- font-family: serif;
- font-size: smaller;
-}
-
.fsflink {
font-size: smaller;
font-family: monospace;
@@ -116,20 +109,6 @@
padding-bottom: 5px;
}
-.trans {
- font-size: smaller;
- color : #000000;
- border-left: #3366cc thin solid;
- padding-left: 20px;
-}
-
-.trans_rtl {
- font-size: smaller;
- color : #000000;
- border-right: #3366cc thin solid;
- padding-right: 20px;
-}
-
img {
border: none 0;
}
@@ -156,11 +135,6 @@
}
-.footnoteref {
- font-size: smaller;
- vertical-align: text-top;
-}
-
/* Please don't remove -- "ss" class is used in Polish pages */
.ss > li, .ss > dt { margin-top: 1em; margin-bottom:0.2em; }
.ss >li > p, .ss > dd > p { margin-top: 0.4em; margin-bottom:0; }
