/**************************************************************************/
/* command prompt */

div.cli {
  font-family: courier-new,monospace;
  font-weight: normal;
  margin: 1em;
  border: 1px solid #A0A0A0;
  padding: 0.5em;
	background-color: #f0f0f0;
}

div.cli span.prompt {
  font-weight: bold;
	color: #206020;
}

div.cli span.typing {
	color: #a02020;
}

div.cli span.response {
	color: #2020f0;
}