// Our customizations to bootstrap go here.

@textColor:             @black;
@baseFontSize:          13px;
@monoFontFamily:        monospace;  // to allow user to customize their fonts
@navbarHeight:          36px;

// Our own global variables for all pages go here

@code_line_height:      1.231em;