It turns out that the gnu.org webmasters while restructuring things
actually broke CSS for the copy of our web pages hosted on www.gnu.org.

This fixes this, and also reduced font size from 80% to 75%.

Gerald

Index: gcc.css
===================================================================
RCS file: /cvs/gcc/wwwdocs/htdocs/gcc.css,v
retrieving revision 1.6
diff -u -r1.6 gcc.css
--- gcc.css     3 Apr 2011 21:45:30 -0000       1.6
+++ gcc.css     4 Apr 2011 15:42:55 -0000
@@ -12,6 +12,15 @@
 
 dl.status dd { margin-left:3ex; }
 
+div.copyright {
+  font-size: 75%;
+  background: #f2f2f9;
+  border: 2px solid #3366cc;
+  border-style: solid;
+  border-width: thin;
+  padding: 4px;
+}
+                  
 /* Classpath versus libgcj merge status page. */
 
 .classpath-only         { background-color: #FFFFAA; }
Index: gnu.css
===================================================================
RCS file: /cvs/gcc/wwwdocs/htdocs/gnu.css,v
retrieving revision 1.7
diff -u -r1.7 gnu.css
--- gnu.css     4 Apr 2011 09:05:44 -0000       1.7
+++ gnu.css     4 Apr 2011 15:42:55 -0000
@@ -44,12 +44,3 @@
        background-color: #f2f2f9;
        font-size: smaller;
 }
-
-div.copyright {
-       font-size: 80%; 
-       border: 2px solid #3366cc; 
-       padding: 4px;
-       background: #f2f2f9;
-       border-style: solid;
-       border-width: thin;
-}

Reply via email to