diff options
-rw-r--r-- | static/style/default.css | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/static/style/default.css b/static/style/default.css index 1b0a029..4c0dd3d 100644 --- a/static/style/default.css +++ b/static/style/default.css @@ -80,14 +80,22 @@ hr { border-right: 55px solid #FFFFFF; } dt { font-weight: bold; } -pre.large { +pre.highlight { font-family: courier; - margin: 10px; + background-color: black; + color: white; + margin: 1em; padding: 6px; - border: 1px solid black; - background-color: #F2D1D1; + border: 2px solid grey; + overflow: auto; } +pre.terminal { + font-family: courier; + background-color: black; + color: white; + margin: 1em; + padding: 6px; + border: 2px solid grey; overflow: auto; } - .search_box { border: 1px solid black; padding: 0.1em; @@ -154,7 +162,8 @@ pre.large { margin-bottom: 0px; padding-left: 24px; padding-right: 24px; - padding-bottom: 12px; } + padding-bottom: 12px; + overflow: hidden; } .content img { border: 1px solid black; } .content_footer { |