/* Increase the default font size */
html {
    font-size: 15pt;
}

/* .toc { */
/*     overflow: scroll; */
/* } */

/* @media (min-width: 1024px) { */
/*     .lg\:sticky { */
/*         position: sticky; */
/*         bottom: 0; */
/*     } */
/*     .lg\:top-10 { */
/*         top: 0; */
/*     } */
/* } */

/* .sticky { */
/*     top: 0; */
/* } */
/**/
/* .toc ul, */
/* .toc li { */
/*     line-height: 0.3; */
/* } */
/**/
/* .toc a { */
/*     font-size: 10pt; */
/* } */
/**/
/* .toc a:hover { */
/*     font-size: 16pt; */
/* } */