div#pager_splitter {
    height: 8px;
}

#pager-container {
    position: relative;
    padding: 15px 0px;
}

div#pager {
    overflow: auto;
    display: none;

    pre {
      font-size: @baseFontSize;
      line-height: @code_line_height;
      color: @textColor;
      background-color: @cell_background;
      padding: 0.4em;
    }
}