diff options
| author | hallgren <hallgren@chalmers.se> | 2011-03-06 10:19:17 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2011-03-06 10:19:17 +0000 |
| commit | 629919667bf2d2c52c6a9a85cbc13397d38ac815 (patch) | |
| tree | e5dfb1fb0adc61613850e0b9bd06a7b2263e96a3 /src/editor/simple/editor.css | |
| parent | f32307b39db77a937aa87b0cd455acc639665cd6 (diff) | |
gfse: minor layout/formatting variation
Diffstat (limited to 'src/editor/simple/editor.css')
| -rw-r--r-- | src/editor/simple/editor.css | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/editor/simple/editor.css b/src/editor/simple/editor.css index 56cfd5adb..a1f48d32c 100644 --- a/src/editor/simple/editor.css +++ b/src/editor/simple/editor.css @@ -27,9 +27,10 @@ td.right { text-align: right; } div.indent { padding-left: 1em; min-width: 1em; min-height: 1em; } +/* div.fun, div.param, div.lincat, div.oper, div.lin { padding-left: 2em; text-indent: -2em; } - +*/ .more, .delete { font-weight: bold; font-family: sans-serif; } .more, .delete, .edit { cursor: pointer; } @@ -71,4 +72,6 @@ table.tabs input[type=button] { font-size: inherit; font-weight: bold; /*text-decoration: underline;*/ -}
\ No newline at end of file +} + +input.string_edit { font-family: inherit; font-size: inherit; }
\ No newline at end of file |