| @import url('https://fonts.googleapis.com/css2?family=Roboto:ital,wght@0,100;0,300;0,400;0,500;0,700;0,900;1,100;1,300;1,400;1,500;1,700;1,900&family=Source+Sans+3:ital,wght@0,200..900;1,200..900&display=swap'); | |
| body { | |
| font-family: 'Roboto'; | |
| } | |
| div#branch-selector { border-right: 1px grey solid; float: right; margin-right: 20pt; padding-right: 20pt; } | |
| div#runtime-fn { float: right; } |