Hi Marcel, On Tue, Dec 06, 2022 at 05:08:10PM +0100, Marcel Fourné wrote: > I just pushed a fix for #1017415 to the group repo and if somebody could > upload it, the package (and therefore the whole agda system) would be > installable again. I tested the agda-mode with a local clean rebuild and an > agda hello world example, which worked fine. > I'm including the original bug reporter to this mail, since they might be > interested to see some progress here.
Thanks for fixing this issue. I confirm that your fix works. I can not only install it, but also use it interatively in emacs again. Thanks. Uploaded. Do you happen to know the DHG processes for tagging this? Helmut
