cerrado @ 6079b1d963f34ada5c4b25363f2319901e283936

  1// disable gutter
  2$grid-gutter-width: 0;
  3
  4$base-font-size: 1rem;
  5$font-family-monospace: monospace;
  6$headings-margin-bottom: 0;
  7
  8// basic functionality
  9@import "bootstrap/scss/_functions.scss";
 10@import "bootstrap/scss/_variables.scss";
 11@import "bootstrap/scss/_variables-dark.scss";
 12@import "bootstrap/scss/_maps.scss";
 13@import "bootstrap/scss/_mixins.scss";
 14@import "bootstrap/scss/_utilities.scss";
 15
 16// added component
 17@import "bootstrap/scss/_root.scss";
 18@import "bootstrap/scss/_containers.scss";
 19@import "bootstrap/scss/_nav.scss";
 20@import "bootstrap/scss/_navbar.scss";
 21@import "bootstrap/scss/_grid.scss";
 22@import "tree.scss";
 23
 24// overwrite to reduce the ammount of css generated by loading all utilities
 25$utilities: (
 26    "order": (
 27      responsive: true,
 28      property: order,
 29      values: (
 30        first: -1,
 31        0: 0,
 32        1: 1,
 33        2: 2,
 34        3: 3,
 35        4: 4,
 36        5: 5,
 37        last: 6,
 38      ),
 39    ),
 40);
 41
 42@import "bootstrap/scss/utilities/_api.scss";
 43
 44body {
 45    // prevents wierd font resizing on overflow
 46    -webkit-text-size-adjust: 100%;
 47    font-family: $font-family-monospace;
 48    font-size: $base-font-size;
 49    margin: 0;
 50}
 51
 52.navbar-nav {
 53  margin-top: 0px
 54}
 55
 56.event-list {
 57    margin-bottom: 1rem;
 58}
 59
 60.event:first-child {
 61    margin-top: 0;
 62}
 63
 64.event {
 65    text-overflow: ellipsis;
 66    overflow: hidden;
 67    padding: 0.5rem;
 68    margin: 0.5rem 0;
 69    background: #f8f9fa;
 70}
 71
 72.selected {
 73  text-decoration: underline;
 74}
 75
 76.event > h4 {
 77  margin: 0;
 78}
 79.event > p {
 80  margin: 0.5rem 0;
 81}
 82
 83.code-view {
 84    display: grid;
 85    overflow-x: auto;
 86}
 87
 88.logs {
 89  >div {
 90    background: #f8f9fa;
 91  }
 92
 93  >div {
 94    padding: 5px;
 95    margin: $spacer;
 96  }
 97
 98  @include media-breakpoint-down(md) {
 99    >div {
100      margin: $spacer 0 $spacer 0;
101    }
102  }
103
104  pre {
105    font-size: $base-font-size;
106    margin: 0;
107  }
108}
109
110.logs>div>div:first-child {
111  margin-bottom: 15px;
112}
113.logs>div>div:last-child {
114  margin-top: 15px;
115}
116
117#about {
118  padding: 0 $spacer $spacer $spacer;
119  > p:first-child {
120    margin-top: 0
121  }
122
123  @include media-breakpoint-down(md) { 
124    padding: $spacer;
125    max-width: calc(100% - calc(2 * #{$spacer}));
126  }
127}