div.cmd {
	color:#000020;
	font-family:courier;
	margin-left:20px;
	margin-bottom:15px;
	white-space:pre;
}