diff options
| -rw-r--r-- | doc/manual/style.css | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/doc/manual/style.css b/doc/manual/style.css index 93ab65c4d138..6c8137ee38f4 100644 --- a/doc/manual/style.css +++ b/doc/manual/style.css @@ -65,22 +65,21 @@ div.refsection h3 /*************************************************************************** - Program listings: + Examples: ***************************************************************************/ div.example { border: 1px solid #6185a0; padding: 6px 6px; - margin-left: 0em; - margin-right: 0em; + margin-left: 1.5em; + margin-right: 1.5em; background: #f4f4f8; } -pre.programlisting +div.example p.title { - color: #600000; - font-family: monospace; + margin-top: 0em; } @@ -100,6 +99,13 @@ pre.screen, pre.programlisting /* font-size: 90%; */ } +div.example pre.programlisting +{ + border: 0px; + padding: 0 0; + margin: 0 0 0 0; +} + /*************************************************************************** Notes, warnings etc: |