3 ms·
Agda highlighting is as uninteresting as it can be. It should be on par of the real Agda highlighting but it is not.
by thesz 12y ago
Agda highlighting is as uninteresting as it can be.
It should be on par of the real Agda highlighting but it is not.
- fijal 12y agoHow about you contribute this missing bit or improve it instead of whining on the internet? This is really a minor feature for pyglets (most people would use it for more mainstream stuff than Agda), so how about you take it over?