@font-face {
	font-family: 'Ubuntu';
	src: url(/fonts/ubuntu-light-webfont.woff2) format('woff2');
	font-weight: 300;
	font-style: normal;
}

@font-face {
	font-family: 'Ubuntu-Mono';
	src: url(/fonts/ubuntumono-regular-webfont.woff2) format('woff2');
	/*font-weight: 300;*/
	font-style: normal;
}

html {
	font-family: Ubuntu, sans-serif;
}

.pure-menu-heading {
	text-transform: none;
	font-family: Ubuntu-Mono,'Noto Mono'
}

.menu-list li a {
	font-family: Ubuntu-Mono,'Noto Mono'
}

.editor {
	border-radius: 6px;
	box-shadow: 0 2px 2px 0 rgba(0, 0, 0, 0.14), 0 1px 5px 0 rgba(0, 0, 0, 0.12), 0 3px 1px -2px rgba(0, 0, 0, 0.2);
	font-family: 'Source Code Pro', monospace;
	font-size: 14px;
	font-weight: 400;
	height: 100%;
	min-height:10%;
	max-height:100%;
	letter-spacing: normal;
	line-height: 20px;
	padding: 10px;
	tab-size: 4;
}

.token.number {
	align-items: initial;
	background-color: initial;
	border-radius: initial;
	display: initial;
	font-size: initial;
	height: initial;
	justify-content: initial;
	margin-right: initial;
	min-width: initial;
	padding: initial;
	text-align: initial;
	vertical-align: initial;
}