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