From edf1c97a978e11d4ab276fec88ada212e4a34b73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?J=C3=A9r=C3=B4me=20Euzenat?= <Jerome.Euzenat@inria.fr>
Date: Sat, 26 Jan 2008 16:48:47 +0000
Subject: [PATCH] - minor changes, certainly
---
html/style.css | 17 ++++++++++++++---
1 file changed, 14 insertions(+), 3 deletions(-)
diff --git a/html/style.css b/html/style.css
index 72d65e9d..1c83119d 100644
--- a/html/style.css
+++ b/html/style.css
@@ -11,10 +11,21 @@ div.owl {
background: #edd;
border:1pt solid;
}
+div.terminal {
+// JE: This may be a bit too much but I like it.
+// Invert color when selecting is not good.
+// I must do something for it to print correctly
+ color: #63FF00;
+ background: #000;
+ font: normal 12px "bitstream vera sans mono", monaco "lucida console", "courier new", courier, serif;
+ overflow: auto;
+}
div.fragment {
- background: #dde;
- border:1pt solid;
- overflow-y: scroll;
+ margin: 0.9em 0; padding: 8px;
+ border: 1pt solid;
+ background: #dde;
+ border:1pt solid;
+ overflow: auto;
}
div.logic {
background: #ded;
--
GitLab