// Our own variables for this page

@cell_selected_background:      darken(@bodyBackground, 2%);
@cell_background:               darken(@bodyBackground, 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