diff options
author | Tor Andersson <tor@ccxvii.net> | 2021-12-19 17:03:16 +0100 |
---|---|---|
committer | Tor Andersson <tor@ccxvii.net> | 2021-12-20 17:43:40 +0100 |
commit | fcc68a8e85c9bd7d76cbb71dece4c6813f3030f0 (patch) | |
tree | a3c652eaa87f9173035ef9bee5d1e22b662e87c0 /public | |
parent | 9ffde5c560301f6bd05e3995b4276d3f802e9b37 (diff) | |
download | server-fcc68a8e85c9bd7d76cbb71dece4c6813f3030f0.tar.gz |
Prettier logs with formatting and colors.
Diffstat (limited to 'public')
-rw-r--r-- | public/common/client.js | 2 | ||||
-rw-r--r-- | public/common/grid.css | 20 |
2 files changed, 9 insertions, 13 deletions
diff --git a/public/common/client.js b/public/common/client.js index 3af9605..dbd719f 100644 --- a/public/common/client.js +++ b/public/common/client.js @@ -315,7 +315,7 @@ let create_log_entry = function (text) { return p; } -let log_scroller = document.querySelector(".grid_log"); +let log_scroller = document.getElementById("log"); function on_update_log() { let parent = document.getElementById("log"); diff --git a/public/common/grid.css b/public/common/grid.css index 09a14eb..657a77f 100644 --- a/public/common/grid.css +++ b/public/common/grid.css @@ -13,7 +13,7 @@ html, button, input, select { font-family: "Source Serif", "Circled Numbers", "Dingbats", "Noto Emoji", "Georgia", serif; } -.log { +#log { font-family: "Source Serif SmText", "Circled Numbers", "Dingbats", "Noto Emoji", "Georgia", serif; } @@ -51,7 +51,7 @@ html { .grid_window.hide_log .grid_role { display: none; } -.grid_window.hide_log .grid_log { +.grid_window.hide_log #log { display: none; } @@ -107,26 +107,22 @@ html { font-family: "Source Serif SmText"; } -.grid_log { +#log { grid-column: 2; grid-row: 3; border-left: 1px solid black; overflow-y: scroll; scrollbar-width: thin; -} - -.log { - padding-left: 20px; - padding-top: 8px; - padding-right: 8px; - padding-bottom: 8px; - text-indent: -12px; + padding: 12px 0; font-size: 12px; line-height: 18px; white-space: pre-wrap; } -.log > * { +#log > * { + padding-left: 20px; + padding-right: 4px; + text-indent: -12px; min-height: 9px; } |