equal
deleted
inserted
replaced
206 .bigtable .size { width: 5em; text-align: right; } |
206 .bigtable .size { width: 5em; text-align: right; } |
207 .bigtable .annotate { text-align: right; } |
207 .bigtable .annotate { text-align: right; } |
208 .bigtable td.annotate { font-size: smaller; } |
208 .bigtable td.annotate { font-size: smaller; } |
209 .bigtable td.source { font-size: inherit; } |
209 .bigtable td.source { font-size: inherit; } |
210 |
210 |
211 .source, .sourcefirst, .sourcelast { |
211 .source, .sourcefirst { |
212 font-family: monospace; |
212 font-family: monospace; |
213 white-space: pre; |
213 white-space: pre; |
214 padding: 1px 4px; |
214 padding: 1px 4px; |
215 font-size: 90%; |
215 font-size: 90%; |
216 } |
216 } |
217 .sourcefirst { border-bottom: 1px solid #999; font-weight: bold; } |
217 .sourcefirst { border-bottom: 1px solid #999; font-weight: bold; } |
218 .sourcelast { border-top: 1px solid #999; } |
|
219 .source a { color: #999; font-size: smaller; font-family: monospace;} |
218 .source a { color: #999; font-size: smaller; font-family: monospace;} |
220 .bottomline { border-bottom: 1px solid #999; } |
219 .bottomline { border-bottom: 1px solid #999; } |
221 |
220 |
222 .sourcelines { |
221 .sourcelines { |
223 font-size: 90%; |
222 font-size: 90%; |