|
@@ -182,7 +182,8 @@ all of MD as it is not optimized for dense, information rich UIs.
|
|
|
--jp-code-font-size: 13px;
|
|
|
--jp-code-line-height: 1.3077; /* 17px for 13px base */
|
|
|
--jp-code-padding: 0.385em; /* 5px for 13px base */
|
|
|
- --jp-code-font-family: 'Source Code Pro', monospace;
|
|
|
+ --jp-code-font-family-default: Menlo, Consolas, 'DejaVu Sans Mono', monospace;
|
|
|
+ --jp-code-font-family: var(--jp-code-font-family-default);
|
|
|
|
|
|
/* This gives a magnification of about 125% in presentation mode over normal. */
|
|
|
--jp-code-presentation-font-size: 16px;
|