[Agda] .lagda.md in emacs interactive mode

Nils Anders Danielsson nad at cse.gu.se
Mon Mar 11 21:12:03 CET 2019


On 11/03/2019 13.39, Martin Escardo wrote:
> When I start emacs with such a file, it doesn't start with the agda
> mode. Do I need to add something to my .emacs?

The Emacs mode currently does not support .lagda.md files:

   https://github.com/agda/agda/issues/2837

-- 
/NAD


More information about the Agda mailing list