Just testing if I can push a commit....

diff --git a/Documentation/texinfo.css b/Documentation/texinfo.css
index 081c9adb9982e0f7939dc2a1c6a60e3f600a772b..af84899fc617053bf99c7e16d7a4963fb1c2079f 100644 (file)
--- a/Documentation/texinfo.css
+++ b/Documentation/texinfo.css
@@ -1 +1,106 @@
   hr { border:0; height:1; color: #000000; background-color: #000000; }
+/* hr {
+  border:  none;
+  height: 1px;
+  color: #666666;
+  background-color: #666666;
+}
+body {
+  border-left: 1px solid #666666;
+  border-right: 1px solid #666666;
+  color: #332d28;
+  margin-right: auto;
+  margin-left: auto;
+  width: 60em;
+  list-style-type: square;
+  font-family: Arial,Helvetica,sans-serif;
+  padding-right: 1em;
+  padding-left: 1em;
+}
+a {
+  border-bottom: 1px dashed #344242;
+  text-decoration: none;
+  color: #344242;
+}
+a:link {
+  text-decoration: none;
+}
+a:visited {
+  border-bottom: 1px dashed #666666;
+  color: #666666;
+}
+a:active {
+  border-bottom: 1px solid #00cccc;
+  color: #00cccc;
+}
+a:hover {
+  border-bottom: 1px solid #1d7b85;
+  color: #1d7b85;
+}
+blockquote {
+  border: 1px solid #cccccc;
+  padding: 3px;
+  width: 40em;
+}
+.node {
+  border-left: 1px solid #666666;
+  margin: -0.5em 0px 1em;
+  padding: 2px 1px 0px;
+  font-style: italic;
+}
+.node a {
+  border:  none;
+  text-decoration: underline;
+  font-style: normal;
+  font-weight: bold;
+}
+.verbatim {
+  font-family: "Courier New",Courier,monospace;
+}
+.unnumberedsubsubsec {
+  font-size: large;
+  color: #1d7b85;
+}
+.subsubheading {
+  font-size: large;
+  color: #3b220d;
+}
+.contents {
+  border: 1px dashed #339999;
+  margin: 3px 2em;
+  list-style-type: square;
+  padding-right: 1em;
+  width: 40em;
+  background-color: #fcfff9;
+}
+.contents a {
+  border-bottom: 1px dashed #423d34;
+  text-decoration: none;
+  color: #423d34;
+}
+.contents a:visited {
+  border-bottom: 1px dashed #666666;
+  color: #666666;
+}
+.contents a:active {
+  border-bottom: 1px solid #f0d86d;
+  color: #f0d86d;
+}
+.contents a:hover {
+  border-bottom: 1px solid #3b220d;
+  color: #3b220d;
+}
+.menu {
+  border-left: 1px dashed #339999;
+  margin: 3px 2em 1em;
+  list-style-type: square;
+  padding-left: 1.4em;
+  width: 40em;
+}
+.unnumbered {
+}
+h2 {
+  font-size: x-large;
+  color: #1d7b85;
+}
+*/