| changeset 68871 | f5c76072db55 |
| parent 67322 | 734a4e44b159 |
| child 69320 | fc221fa79741 |
| 68870:53a75627aab7 | 68871:f5c76072db55 |
|---|---|
11 /* known decoration types */ |
11 /* known decoration types */ |
12 |
12 |
13 const background_colors = [ |
13 const background_colors = [ |
14 "unprocessed1", |
14 "unprocessed1", |
15 "running1", |
15 "running1", |
16 "canceled", |
|
16 "bad", |
17 "bad", |
17 "intensify", |
18 "intensify", |
18 "quoted", |
19 "quoted", |
19 "antiquoted", |
20 "antiquoted", |
20 "markdown_bullet1", |
21 "markdown_bullet1", |