Make the font size of Agda buffer the same as editors - Githubissues

banacorn / agda-mode-vscode

agda-mode on VS Code

https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode

MIT License

167 stars 38 forks source link

Make the font size of Agda buffer the same as editors #167

Closed vic0103520 closed 10 months ago

vic0103520 commented 10 months ago

As the title

L-TChen commented 10 months ago

Thanks!