Revert CSS changes accidentally committed

jonludlam · jonludlam · commit 88167284a74a · 2021-10-01T19:20:55.000+01:00
diff --git a/src/odoc/etc/odoc.css b/src/odoc/etc/odoc.css
@@ -399,10 +399,6 @@ li code {
   padding: 0 0.3ex;
 }
 
-li a code {
-  color: var(--link-color);
-}
-
 p a > code {
   color: var(--link-color);
 }
@@ -432,8 +428,7 @@ pre code {
 }
 
 div.spec, .def-doc {
-  margin-top: 20px;
-  margin-bottom: 10px;
+  margin-bottom: 20px;
 }
 
 .spec.type .variant {
@@ -523,10 +518,6 @@ td.def-doc *:first-child {
   margin-top: 0em;
 }
 
-td.def-doc {
-  padding-left: 2ex;
-}
-
 /* Lists of @tags */
 
 .at-tags { list-style-type: none; margin-left: -3ex; }

Original file line number	Diff line number	Diff line change
`@@ -399,10 +399,6 @@ li code {`
`399`	`399`	`padding: 0 0.3ex;`
`400`	`400`	`}`
`401`	`401`
`402`		`-li a code {`
`403`		`- color: var(--link-color);`
`404`		`-}`
`405`		`-`
`406`	`402`	`p a > code {`
`407`	`403`	`color: var(--link-color);`
`408`	`404`	`}`
`@@ -432,8 +428,7 @@ pre code {`
`432`	`428`	`}`
`433`	`429`
`434`	`430`	`div.spec, .def-doc {`
`435`		`- margin-top: 20px;`
`436`		`- margin-bottom: 10px;`
	`431`	`+ margin-bottom: 20px;`
`437`	`432`	`}`
`438`	`433`
`439`	`434`	`.spec.type .variant {`
`@@ -523,10 +518,6 @@ td.def-doc *:first-child {`
`523`	`518`	`margin-top: 0em;`
`524`	`519`	`}`
`525`	`520`
`526`		`-td.def-doc {`
`527`		`- padding-left: 2ex;`
`528`		`-}`
`529`		`-`
`530`	`521`	`/* Lists of @tags */`
`531`	`522`
`532`	`523`	`.at-tags { list-style-type: none; margin-left: -3ex; }`