You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
18 lines
752 B
18 lines
752 B
|
|
// Our own variables for this page
|
|
|
|
@cell_selected_background: darken(@body-bg, 2%);
|
|
@cell_background: darken(@body-bg, 3.2%);
|
|
@border_color: darken(@cell_selected_background, 31%);
|
|
@light_border_color: darken(@cell_selected_background, 17%);
|
|
@border_width: 1px;
|
|
@notebook_font_size: 14px;
|
|
@notebook_line_height: 20px;
|
|
@code_line_height: 1.21429em; // changed from 1.231 to get 17px even
|
|
@code_padding: 0.4em; // 5.6 px
|
|
@rendered_html_border_color: black;
|
|
@input_prompt_color: navy;
|
|
@output_prompt_color: darkred;
|
|
@output_pre_color: black;
|
|
@notification_widget_bg: rgba(240, 240, 240, 0.5);
|