change header of references pane to show heading instead of anchor#542

Merged

bakkot merged 4 commits intomainfrom references-shows-title

Aug 30, 2023

+5-7

Commits on Aug 26, 2023

change header of references pane to show heading instead of anchor

michaelficarra
authored and
bakkot
committed
support all reference-able things

michaelficarra
authored and
bakkot
committed
update styles a bit

michaelficarra
authored and
bakkot
committed

Commits on Aug 30, 2023

Merge branch 'main' into references-shows-title
bakkot
authored