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

[Andrés Sicard-Ramírez]

Hi,

After showing a nice Agda logo in ASCII, the command

  $ agda --interactive

says

  The interactive mode is no longer supported. Don't complain if it doesn't
work.

​
I propose to remove the --interactive option and its associated module
Agda.Interaction.CommandLine.CommandLine (actually, I propose to comment
out the related code).

Why? While fixing new bugs (e.g.
https://github.com/agda/agda/commit/8631ef270c387e6639873bafba8259247d76cba0)
and supporting various versions of GHC and libraries, why lost time maintaining
a option whose functionality is not maintained?

​My idea is remove the option from both branches (I know it isn't a
bug-fix).
​
I will also ask in the Agda mailing list before removing the option.

​Comments?​

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