From 266e5eccce217771ae119c78e2d8a5abb22ec5d3 Mon Sep 17 00:00:00 2001 From: ansuz Date: Mon, 1 Feb 2016 14:14:32 +0100 Subject: [PATCH] change styles for rendered page --- www/render/index.html | 11 ++++++++--- www/render/main.js | 2 -- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/www/render/index.html b/www/render/index.html index 8ef32b30d..7b1794dd1 100644 --- a/www/render/index.html +++ b/www/render/index.html @@ -8,15 +8,13 @@ html, body { padding: 0px; margin: 0px; + box-sizing: border-box; } #target { position: fixed; - box-sizing: border-box; - border: 1px solid blue; width: 100%; height: 100%; overflow: auto; - font-size: 15px; top: 0px; left: 0px; @@ -32,6 +30,13 @@ img { max-width: 100%; } + /* monospace for code */ + code { + font-family: monospace; + } + /* TODO + bump up text size on mobile + */ diff --git a/www/render/main.js b/www/render/main.js index 511035216..6f1825262 100644 --- a/www/render/main.js +++ b/www/render/main.js @@ -120,8 +120,6 @@ define([ return rt; })[0]; - window.rts = rts; - $textarea.on('change keyup keydown', function () { redrawTimeout && clearTimeout(redrawTimeout); redrawTimeout = setTimeout(function () {