diff --git a/doc/index.html b/doc/index.html index ae2c76e4cc..758f02f8e5 100644 --- a/doc/index.html +++ b/doc/index.html @@ -30,9 +30,10 @@
  • Wiki
  • Blog
  • -
  • Jobs
  • Community
  • Demo
  • +
  • Jobs
  • +
    diff --git a/doc/pipe.css b/doc/pipe.css index c86bf2ae36..5d9edfea4b 100644 --- a/doc/pipe.css +++ b/doc/pipe.css @@ -15,7 +15,7 @@ img { position: absolute; top: 2em; left: 0; - width: 8em; + width: 10em; font-size: 12pt; line-height: 150%; } @@ -42,6 +42,12 @@ h1, h2, h3, h4 { margin: 2em 0; } +#toc ol ol { + font-size: 8pt; + line-height: 110%; + list-style: circle; +} + h1 code, h2 code, h3 code, h4 code, h1 a, h2 a, h3 a, h4 a {