##// END OF EJS Templates
Remove right margin from the terminal
Jonathan Frederic -
Show More
@@ -10473,6 +10473,9 b' span.autosave_status {'
10473 10473 color: white;
10474 10474 background: black;
10475 10475 padding: 0.4em;
10476 border-radius: 2px;
10477 -webkit-box-shadow: 0px 0px 12px 1px rgba(87, 87, 87, 0.4);
10478 box-shadow: 0px 0px 12px 1px rgba(87, 87, 87, 0.4);
10476 10479 }
10477 10480 .terminal,
10478 10481 .terminal dummy-screen {
@@ -10485,9 +10488,5 b' span.autosave_status {'
10485 10488 }
10486 10489 #terminado-container {
10487 10490 margin-top: 20px;
10488 background: black;
10489 border-radius: 2px;
10490 -webkit-box-shadow: 0px 0px 12px 1px rgba(87, 87, 87, 0.4);
10491 box-shadow: 0px 0px 12px 1px rgba(87, 87, 87, 0.4);
10492 10491 }
10493 10492 /*# sourceMappingURL=style.min.css.map */ No newline at end of file
@@ -4,6 +4,8 b''
4 4 color: white;
5 5 background: black;
6 6 padding: @code_padding;
7 border-radius: @border-radius-base;
8 .box-shadow(@global-shadow-dark);
7 9
8 10 &, dummy-screen {
9 11 line-height: 1em;
@@ -18,7 +20,4 b''
18 20
19 21 #terminado-container {
20 22 margin-top: @page-header-padding;
21 background: black;
22 border-radius: @border-radius-base;
23 .box-shadow(@global-shadow-dark);
24 23 }
General Comments 0
You need to be logged in to leave comments. Login now