Skip to content

Add definition summary hovers on diffs#128

Merged
hojberg merged 1 commit intomainfrom
diff-hover
Oct 30, 2025
Merged

Add definition summary hovers on diffs#128
hojberg merged 1 commit intomainfrom
diff-hover

Commits

Commits on Oct 30, 2025