##// END OF EJS Templates
MAINT: Return dicts from CheckpointManager.get_checkpoint....
MAINT: Return dicts from CheckpointManager.get_checkpoint. The output is going to get converted to a dict anyway, and this makes it easier to pipe output from a CheckpointManager directly to a ContentsManager.

File last commit:

r19664:24be0d51
r19825:f587966f
Show More
edit.less
34 lines | 772 B | text/x-less | LessCssLexer
#filename {
font-size: 16pt;
display: table;
padding: 0px 5px;
}
#texteditor-backdrop {
padding-top: @page-header-padding;
padding-bottom: @page-header-padding;
@media not print{
min-height: @page-backdrop-height;
background-color: @page-backdrop-color;
}
#texteditor-container {
.CodeMirror-gutter, .CodeMirror-gutters {
@media print {
background-color: @body-bg;
}
@media not print {
background-color: @page-color;
}
}
@media not print{
padding: 0px;
background-color : @page-color;
min-height: @page-min-height;
.box-shadow(@global-shadow);
}
}
}