Workaround to fix #78

sharkdp · Jul 1, 2017 · 733fad1 · 733fad1
1 parent ae9970d
commit 733fad1
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/index.html b/index.html
@@ -86,7 +86,7 @@
           greetings: greeting,
           name: "terminal",
           height: 550,
-          prompt: emph("&#8811; "),
+          prompt: "[[;;;prompt]&#8811; ]",
           clear: false, // do not include 'clear' command
           exit: false, // do not include 'exit' command
           checkArity: false,

diff --git a/main.css b/main.css
@@ -35,6 +35,13 @@ p.desc {
     box-shadow: 0px 3px 8px #1a1a1a;
 }
 
+/* jQuery Terminal */
+.prompt {
+    font-weight: bold;
+    /* workaround for https://github.com/sharkdp/insect/issues/78 */
+    letter-spacing: 1px;
+}
+
 /* syntax highlighting */
 
 .hl-emphasized {