From 1ea15ca236849870199ea3ecf3b3279d2e53abe1 Mon Sep 17 00:00:00 2001
From: Martin Fischer <fischer.carlito@gmail.com>
Date: Sat, 14 May 2016 18:11:25 +0200
Subject: [PATCH] terminal: change font size automatically

font size is proportional to viewport, so it scales and is better readable on high
resolution screens
---
 webrepl.html | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/webrepl.html b/webrepl.html
index 88d384f..39f43a0 100644
--- a/webrepl.html
+++ b/webrepl.html
@@ -17,16 +17,15 @@
     font: 20px/1.5 sans-serif;
   }
 
-/*
   .terminal {
     float: left;
     border: #000 solid 5px;
     font-family: "DejaVu Sans Mono", "Liberation Mono", monospace;
-    font-size: 11px;
+    font-size: 1.2vw;
     color: #f0f0f0;
     background: #000;
   }
-
+/*
   .terminal-cursor {
     color: #000;
     background: #f0f0f0;