From c67cdd5b301bee08cab6d3cb3a0766578972c08c Mon Sep 17 00:00:00 2001
From: William S Fulton <wsf@fultondesigns.co.uk>
Date: Wed, 16 Apr 2014 07:59:24 +0100
Subject: [PATCH] Revert css style changes in javascript branch

---
 Doc/Manual/style.css | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Doc/Manual/style.css b/Doc/Manual/style.css
index 7eabf91ae..02329e56f 100644
--- a/Doc/Manual/style.css
+++ b/Doc/Manual/style.css
@@ -25,7 +25,7 @@ div.indent {
   margin-right: 4em;
 }
 
-div.code, div:not(.code) pre {
+div.code {
   border-style: solid; 
   border-width: 1px; 
   padding: 2pt; 
@@ -82,7 +82,3 @@ div.indent p {
   margin-right: 0;
 }
 
-h1 a, h2 a, h3 a, h4 a, h5 a, h6 a {
-  text-decoration:none;
-  color: #000000;
-}