search

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

Custom Agda buffer font size in the extension's setting #169

Open vic0103520 opened 9 months ago

vic0103520 commented 9 months ago

As title.

It seems that CI on Windows failed before testing since it cannot download vscode. Is there any solution? CI

L-TChen commented 9 months ago

The package vscode-test is outdated and has been renamed to @vscode/test-electron. I am trying upgrading it on my fork https://github.com/L-TChen/agda-mode-vscode.