Open Issues Need Help
View All on GitHub Can't toggle Agda comments under markup comments in literate Agda files about 2 months ago
AI Summary: The task is to investigate and fix a bug in the VS Code agda-mode extension where toggling Agda comments within HTML comments in literate Agda files (.lagda.md) does not function correctly. This involves debugging the extension's comment handling to ensure it correctly identifies and processes comments nested within other comment types.
Complexity:
4/5
bug enhancement help wanted
agda-mode on VS Code
ReScript
#agda#agda-mode#reasonml#vscode#vscode-extension