##// END OF EJS Templates
use baseBorderRadius instead of corner_radius...
Matthias BUSSONNIER -
Show More
@@ -7,5 +7,5 b''
7 }
7 }
8
8
9 .corner-all {
9 .corner-all {
10 border-radius: @corner_radius;
10 border-radius: @baseBorderRadius;
11 } No newline at end of file
11 }
@@ -7,5 +7,4 b''
7
7
8 // Our own global variables for all pages go here
8 // Our own global variables for all pages go here
9
9
10 @corner_radius: 4px;
11 @code_line_height: 1.231em;
10 @code_line_height: 1.231em;
@@ -45,8 +45,8 b''
45 .CodeMirror-gutters {
45 .CodeMirror-gutters {
46 // This is needed because our cell has rounded corners, otherwise the gutter area square
46 // This is needed because our cell has rounded corners, otherwise the gutter area square
47 // corner cuts into the rounded cell border.
47 // corner cuts into the rounded cell border.
48 border-bottom-left-radius: @corner_radius;
48 border-bottom-left-radius: @baseBorderRadius;
49 border-top-left-radius: @corner_radius;
49 border-top-left-radius: @baseBorderRadius;
50 }
50 }
51
51
52 .CodeMirror pre {
52 .CodeMirror pre {
@@ -4,7 +4,7 b''
4 margin: 2px 4px;
4 margin: 2px 4px;
5 z-index: 10;
5 z-index: 10;
6 border: 1px solid #ccc;
6 border: 1px solid #ccc;
7 border-radius: @corner_radius;
7 border-radius: @baseBorderRadius;
8 background: rgba(240, 240, 240, 0.5);
8 background: rgba(240, 240, 240, 0.5);
9
9
10 }
10 }
General Comments 0
You need to be logged in to leave comments. Login now