body { padding:30px; margin-bottom:80px;}
h1,h2 { margin-left:20px; margin-right:20px; margin-top:40px; }
h3 { margin-left:25px; margin-right:20px; }
h4 { margin-left:30px; margin-right:20px; }
p { margin-left:40px; margin-right:40px;font-size:12pt; }
img { margin-left:auto; margin-right:auto; }
li { margin-left:40px; margin-right:40px; margin-top:9px; margin-bottom:6px;}
li li { margin-left:10px; margin-right:40px; margin-top:9px; margin-bottom:6px;}
.game { margin-left:80px; 
    font-family:monospace; font-size:12pt; white-space:pre;}
dt { margin-left:60px; margin-right:40px; margin-top:20px; margin-bottom:2px;
    font-weight:bold;}
dd { margin-left:80px; margin-right:40px; margin-top:9px; margin-bottom:6px;}
dd > br { margin-bottom:10px; }
.pts { font-size:14pt;color:darkred; }
.smallpts { font-size:12pt;color:darkred; }
tt { font-size:11pt; }
.cmdline { margin-left:50px;font-size:12pt; }
pre {
    margin-left:50px;font-size:12pt;
    border:1px solid;
    background-color:#e4e4e4;
    white-space:pre;
    font-family:monospace;
    padding-top:10px;
    padding-bottom:10px;
    padding-left:20px;
    padding-right:20px;
    margin-right:50px;
}
.file { 
    font-size:9pt;
    background-color:#f6f6f6;
}
.change { color:#cc0000; }
.cite { margin-left:120px; margin-right:120px; }

table {
    width:calc(100% - 160px);
    margin-left:80px;
    margin-right:80px;
}
th,td { padding:6px;border:1px solid black }

/* Operating-system-specific instructions */

.os-linux,
.os-linux * {
    color: red !important;
}

.os-macos,
.os-macos * {
    color: #009b00 !important;
}

.os-windows,
.os-windows * {
    color: #000080 !important;
}

div.sourceCode {
    margin-left: 50px;
    margin-right: 50px;
}

.xp {
    color: #8B0000;
    font-weight: bold;
}

.box {
    margin-left:120px;
    margin-right:120px;
    border:1px solid;
    background-color:#fffacd;
    padding:10px 20px;
}