[Agda-dev] Proposal: Remove the --interactive option

[Andrés Sicard-Ramírez]

On 12 February 2015 at 14:57, Ulf Norell <ulf.norell at gmail.com> wrote:

> I remember that some people objected when I tried to get rid of it a few
> years ago.


​​
Let's see what happens
​now
.​

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150212/bb8f1c5f/attachment.html