[Agda] Poll: Remove the Agda interactive mode

[Andreas Abel]

Note:

   --interaction is emacs communication

   --interactive or -I is the ghci-like interface

Well-chosen names... ;-)

On 13.02.2015 20:44, Mateusz Kowalczyk wrote:
> 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?
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/