search

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

Debug buffer prints more then necessary #90

Open L-TChen opened 2 years ago

L-TChen commented 2 years ago

The debug buffer prints

  1. modules being checked and
  2. a number
Screenshot 2022-01-22 at 11 35 58

apart from the actual information printed to the debug buffer. Can you remove these two parts?

L-TChen commented 2 years ago

By the way, the output in Emacs does not contain these two kinds of information.