expand error line widgets on mouse over

2026-04-20 00:17:04 +00:00 · 2018-07-26 15:47:09 -04:00
parent 24693ac6eb
commit 0e807690e8
8 changed files with 38 additions and 33 deletions
@@ -24,6 +24,7 @@ body {
 </div>

 <div id="notebook">
+  <!-- TODO: doesn't work properly when screen isn't exactly centered -->
  <div id="thumbnaildiv" style="float:right;margin-top:20%;transform:scale(2);margin-right:10%">
  </div>
  <div id="maineditor" style="height:100%">