body { padding: 2em; background-color: #FFFFFF; }
       margin: 0 1em 0 1em; }
dl   { margin: 1em 2em 0 2em; }
pre  { line-height: 100%; margin: 0.5em;}
div.shell { border: 0.5em groove; background-color: #000000;
          margin: 0; color: #FFFFFF; 
          border-color: #000000; }
div.script { border: 0.5em groove; background-color: #efefe0;
          margin: 0; color: #000000; 
          border-color: #000000; }