diff options
Diffstat (limited to 'src/www/gfse/editor.css')
| -rw-r--r-- | src/www/gfse/editor.css | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/www/gfse/editor.css b/src/www/gfse/editor.css index 28712e500..27a589a1f 100644 --- a/src/www/gfse/editor.css +++ b/src/www/gfse/editor.css @@ -17,10 +17,16 @@ div.home, div.grammar { border: 1px solid black; background: #9df; } div.home { padding: 5px; } div.files { margin: 0 8px 8px 8px; } -div#file { border: 2px solid #009; border-top-width: 0; } +div#file, table.extension td, table.extension th { border: 2px solid #009 } +div#file { border-top-width: 0; } pre.plain { border: 2px solid #009; } div#file, pre.plain { background: white; padding: 0.6ex; } +table.extension { border-collapse: collapse; background: white; } +table.extension td, table.extension th { padding: 1ex; } +table.extension th { border-right-width: 0; color: #009; } +table.extension td { border-left-width: 0; } + .slideshow .hidden { display: none; } img.cloud, img.right, div.right, div.modtime { float: right; } |
