mathlib
861f1821
- feat(widget): add go to definition button. (#3982)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
feat(widget): add go to definition button. (#3982) Now you can hit a new button in the tooltip and it will reveal the definition location in the editor! Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
References
#4925 - Make prime-avoidance branch build
Author
EdAyers
Parents
f9ee4166
Loading