[Agda] Poll: Remove the Agda interactive mode

[Mateusz Kowalczyk]

On 02/13/2015 04:17 AM, Andrés Sicard-Ramírez wrote:
> Hi,
> 
> ​For simplifying the support of various versions of GHC and Haskell
> libraries, and the bug fixing process, we might consider to remove the Agda
> (not Emacs) interactive mode, i.e. the mode called using the --interactive
> option. Note that this mode is not currently supported.
> 
> If you are using the Agda interactive mode, please reply this message.
> 
> Best,
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

Is --interactive not used by emacs? What would change there
implementation-wise?

-- 
Mateusz K.