banacorn / agda-mode-vscode

agda-mode on VS Code

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

MIT License

169 stars 39 forks source link

Agda files are not Markdown files #124

Closed plt-amy closed 1 year ago

plt-amy commented 1 year ago

121 highlights all Agda files (Agda, TeX, rST, etc) as though they were Markdown. They are not

L-TChen commented 1 year ago

Fixed by #148.