Source

coveragepy / coverage / htmlfiles / definitions.less

Full commit
/*
 * definitions.less: Style variable definitions.
 */

/* Colors */
// Base colors
@color-white: #fff;
@color-light-smoke: #f2f2f2;

// Header
@color-header-gradient-top: #f4f4f4;
@color-header-gradient-bottom: #e5e5e5;
@color-header-border-top: @color-white;
@color-header-border-bottom: #d2d2d2;
@color-header-box-shadow: #888;

// Line numbers.
@color-line-number-text: #999; // #77C;


// Chrome buttons.
@color-chrome-button-box-shadow: rgba(0, 0, 0, 0.1);

@color-chrome-button-gradient-top: #fafafa;
@color-chrome-button-gradient-bottom: #e5e5e5;
@color-chrome-button-background: darken(#f2f2f2, 5%);
@color-chrome-button-border: #aaa;
@color-chrome-button-text: #444;

@color-chrome-button-gradient-top-active: @color-chrome-button-gradient-bottom;
@color-chrome-button-gradient-bottom-active: @color-chrome-button-gradient-top;
@color-chrome-button-text-active: @color-chrome-button-text;

@color-chrome-button-gradient-top-hover: @color-white;
@color-chrome-button-gradient-bottom-hover: #f4f4f4; //@color-chrome-button-gradient-top;
@color-chrome-button-background-hover: @color-light-smoke;
@color-chrome-button-text-hover: #222;
@color-chrome-button-border-hover: #888;

@color-chrome-button-gradient-top-checked: #666;
@color-chrome-button-gradient-bottom-checked: #888;
@color-chrome-button-border-top-checked: #555;
@color-chrome-button-border-bottom-checked: #777;
@color-chrome-button-text-checked: @color-light-smoke;

@color-chrome-button-gradient-top-disabled: #dcdcdc;
@color-chrome-button-gradient-bottom-disabled: #aaa;
@color-chrome-button-text-disabled: #888;
@color-chrome-button-text-shadow-disabled: #fafafa;

/* Typography */
@font-family-ui: "Lucida Grande", "Droid Sans", "Helvetica", "Verdana", sans-serif;
@font-family-code: "Monaco", "Consolas", "Inconsolata", "Anonymous", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Lucida Console", monospace;
@font-family-text: "Droid Serif", "Georgia", serif;
@font-family-line-number-text: @font-family-ui; // @font-family-code;