/* the class shell is used when a copy of the content of a shell or DOS window is made */
.shell {background-color: black; color: white; border: medium gray solid;}
.shell pre {background-color: black; border: none; font-size: small;}