div#pager_splitter {
    height: 8px;
    .border-box-sizing();
}

#pager-container {
    position: relative;
    padding: 15px 0px;
    .border-box-sizing();
}

div#pager {
    font-size: @notebook_font_size;
    line-height: @notebook_line_height;
    overflow: auto;
    display: none;

    pre {
      line-height: @code_line_height;
      color: @text-color;
      background-color: @cell_background;
      padding: @code_padding;
    }
    .border-box-sizing();
}