diff options
author | Hans Hagen <pragma@wxs.nl> | 2014-09-18 11:17:00 +0200 |
---|---|---|
committer | Hans Hagen <pragma@wxs.nl> | 2014-09-18 11:17:00 +0200 |
commit | ea8cd771135d573fee6529e62e08468e79b12eab (patch) | |
tree | d2f7102bac47807fd3a0cbfeb02a0bb2f6f13a30 /tex/context/base/export-example.css | |
parent | 02d4d3cbde5e1e94e056cdf3b732145a37413fdb (diff) | |
download | context-ea8cd771135d573fee6529e62e08468e79b12eab.tar.gz |
beta 2014.09.18 11:17
Diffstat (limited to 'tex/context/base/export-example.css')
-rw-r--r-- | tex/context/base/export-example.css | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/tex/context/base/export-example.css b/tex/context/base/export-example.css index 10db21982..f78014a5d 100644 --- a/tex/context/base/export-example.css +++ b/tex/context/base/export-example.css @@ -50,7 +50,7 @@ document, div.document { } document>metadata, div.document div.metadata { - font-family : "Lucida Console", "DejaVu Sans Mono", monospace ; + font-family : "DejaVu Sans Mono", "Lucida Console", monospace ; margin-bottom : 2em ; } @@ -312,7 +312,7 @@ verbatimblock, div.verbatimblock { padding : 1em ; margin-bottom : 1em ; margin-top : 1em ; - font-family : "Lucida Console", "DejaVu Sans Mono", monospace ; + font-family : "DejaVu Sans Mono", "Lucida Console", monospace ; } verbatimlines+verbatimlines, div.verbatimlines+div.verbatimlines { @@ -329,7 +329,7 @@ verbatim, div.verbatim { display : inline ; white-space : pre-wrap ; color : rgb(60%,60%,0%) ; - font-family : "Lucida Console", "DejaVu Sans Mono", monospace ; + font-family : "DejaVu Sans Mono", "Lucida Console", monospace ; } /* lines : display */ @@ -773,7 +773,17 @@ comment, div.comment { background-color : rgb(50%,75%,100%) ; display : block ; padding : 1em ; - margin-bottom : 1em ; - margin-top : 1em ; - font-family : "Lucida Console", "DejaVu Sans Mono", monospace ; + margin-bottom : 2ex ; + margin-top : 2ex ; + font-family : "DejaVu Sans Mono", "Lucida Console", monospace ; +} + +/* special */ + +c, div.c { + display : inline ; +} + +warning, div.warning { + display : none ; } |