Explorar el Código

Fix handling of monospace font in terminal

Steven Silvester hace 8 años
padre
commit
d83c9d3e75
Se han modificado 1 ficheros con 1 adiciones y 1 borrados
  1. 1 1
      src/terminal/index.css

+ 1 - 1
src/terminal/index.css

@@ -15,7 +15,7 @@
 
 
 .jp-TerminalWidget-body {
- font-family: "DejaVu Sans Mono", "Liberation Mono", monospace;
+  font-family: monospace;
   outline: none;
   user-select: text;
   -webkit-user-select: text;