Doc: Push small CSS fix

hammerlab · Feb 26, 2020 · 8262ad8 · 8262ad8
1 parent 263c0a3
commit 8262ad8
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/tools/build-doc.sh b/tools/build-doc.sh
@@ -25,6 +25,7 @@ css_path=$output_path/$css_file
 cat >> $output_path/odoc.css <<EOF
 body {
   max-width: 72em; /* A bit larger than odoc's output */
+  margin-left: 4em;
 }
 EOF
 cat $output_path/odoc.css > $css_path