Skip to content

Commit 8f1aa7c

Browse files
authored
web: add CSS rule for macro names (#397)
agda/agda#7325
1 parent 9b594c4 commit 8f1aa7c

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

support/web/css/code.scss

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,7 @@ a[href].hover-highlight {
9999

100100
.Datatype { color: theme(--primary) !important; }
101101
.Function { color: theme(--primary) !important; }
102+
.Macro { color: theme(--primary) !important; }
102103
.Postulate { color: theme(--primary) !important; }
103104
.Primitive { color: theme(--primary) !important; }
104105
.Record { color: theme(--primary) !important; }

0 commit comments

Comments
 (0)