diff options
Diffstat (limited to 'manual.css')
-rw-r--r-- | manual.css | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/manual.css b/manual.css new file mode 100644 index 0000000..570c4ef --- /dev/null +++ b/manual.css @@ -0,0 +1,50 @@ +html { + background-color : white; + color : black; + font-family : sans-serif; +} + +p, ul, ol, dl, .example { + margin-top : 0.5em; + margin-bottom : 0.5em; +} + +pre, code { + font-family : monospace; +} + +pre { + white-space : pre-wrap; +} + +pre.make { + white-space : pre; +} + +.example { + display : table; + margin-left : 2em; + margin-right : 2em; + background-color : #EEEEEE; + padding : 0.2em; +} + +.file { + border-color : #DDDDDD; + border-width : thin; + border-style : solid; + padding : 0; +} + +.file > * { + margin : 0; + padding : 0.2em; +} + +.file > *:first-child { + background-color : #DDDDDD; + font-size : inherit; + font-variant : inherit; + font-style : inherit; + font-weight : bolder; +} |