cerrado @ 89705dd61f418df561ebbe7cf645ba82a61e47e7

  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  "float": (
 41    responsive: true,
 42    property: float,
 43    values: (
 44      start: left,
 45      end: right,
 46      none: none,
 47    )
 48  ),
 49);
 50
 51@import "bootstrap/scss/utilities/_api.scss";
 52
 53body {
 54    // prevents wierd font resizing on overflow
 55    -webkit-text-size-adjust: 100%;
 56    font-family: $font-family-monospace;
 57    font-size: $base-font-size;
 58    margin: 0;
 59}
 60
 61.navbar-nav {
 62  margin-top: 0px
 63}
 64
 65.event-list {
 66    margin-bottom: 1rem;
 67}
 68
 69.event:first-child {
 70    margin-top: 0;
 71}
 72
 73.event {
 74    text-overflow: ellipsis;
 75    overflow: hidden;
 76    padding: 0.5rem;
 77    margin: 0.5rem 0;
 78    background: #f8f9fa;
 79}
 80
 81.selected {
 82  text-decoration: underline;
 83}
 84
 85.event > h4 {
 86  margin: 0;
 87}
 88.event > p {
 89  margin: 0.5rem 0;
 90}
 91
 92.code-view {
 93    display: grid;
 94    overflow-x: auto;
 95}
 96
 97.logs {
 98  >div {
 99    background: #f8f9fa;
100  }
101
102  >div {
103    padding: 5px;
104    margin: $spacer;
105  }
106
107  @include media-breakpoint-down(md) {
108    >div {
109      margin: $spacer 0 $spacer 0;
110    }
111  }
112
113  pre {
114    font-size: $base-font-size;
115    margin: 0;
116  }
117}
118
119.logs>div>div:first-child {
120  margin-bottom: 15px;
121}
122.logs>div>div:last-child {
123  margin-top: 15px;
124}
125
126#about {
127  padding: 0 $spacer $spacer $spacer;
128  > p:first-child {
129    margin-top: 0
130  }
131
132  @include media-breakpoint-down(md) { 
133    padding: $spacer;
134    max-width: calc(100% - calc(2 * #{$spacer}));
135  }
136}