[Agda] --termination-depth

[Sergei Meshveliani]

On Thu, 2015-03-05 at 11:51 -0500, Andrés Sicard-Ramírez wrote:
> On 5 March 2015 at 10:28, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > But before this, I tried   --termination-depth=4.
> > And this does not help.
> >
> > 1) Is this option for this case?
> 
> AFAIK, this option is obsolete (see
> https://github.com/agda/agda/commit/1ac6343c42b295649d6e66995fdf4e317d816630).
> 

If it is obsolete, then Agda probably needs to report this explicitly.

------
Sergei