aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJohn MacFarlane <jgm@berkeley.edu>2014-10-28 11:54:10 -0700
committerJohn MacFarlane <jgm@berkeley.edu>2014-10-28 11:54:10 -0700
commit2de98358a54fe35f584e30181d86460bb842ebee (patch)
tree3c8e102f9a8111d0cb72480c6921e463af524c95
parent022bdd91a161078e88a11502fcbb39907bf78ecc (diff)
More dingus refinements.
changes. Lines starting
-rw-r--r--dingus.html7
1 files changed, 4 insertions, 3 deletions
diff --git a/dingus.html b/dingus.html
index 3c418bf..bb26460 100644
--- a/dingus.html
+++ b/dingus.html
@@ -94,10 +94,11 @@ $(document).ready(function() {
<style type="text/css">
h1.title { font-family: monospace; font-size: 120%; font-weight: bold;
margin-top: 0.5em; margin-bottom: 0; }
- textarea#text { min-height: 400px; width: 95%; font-family: monospace; font-size: 92%; }
+ textarea#text { height: 400px; width: 95%; font-family: monospace; font-size: 92%; }
pre code#html { font-size: 92%; font-family: monospace; }
- pre#htmlpre { min-height: 400px; resize: vertical; width: 95%; overflow: scroll; }
- div#preview { min-height: 400px; resize: vertical; width: 95%; overflow: scroll; }
+ pre#htmlpre { height: 400px; overflow: scroll; resize: vertical; width: 95%; }
+ div#astpre { height: 400px; overflow: scroll; resize: vertical; width: 95%; }
+ div#preview { height: 400px; overflow: scroll; resize: vertical; width: 95%; }
div.row { margin-top: 1em; }
blockquote { font-size: 100%; }
footer { color: #555; text-align: center; margin: 1em; }