[Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2
Sergei Meshveliani
mechvel at botik.ru
Thu Apr 14 15:42:48 CEST 2016
On Thu, 2016-04-14 at 08:25 -0500, Andrés Sicard-Ramírez wrote:
> On 14 April 2016 at 06:38, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > 3. I try
> > agda -c $agdaLibOpt +RTS -M9G -RTS Foo.agda
> >
> > ./Foo +RTS -M2G -RTS
> >
> > , and it reports "link with the -rtsopts".
>
> Did it work before?
>
> > Please, how precisely needs one to use -rtsopts ?
>
> The -rtsopts option should be used by the GHC backend when generating
> the Foo executable.
>
I am sorry.
I recall now how to use it. This is to add
--ghc-flag=-rtsopts
to the `agda -c' command.
This makes it "linking with -rtsopts".
Regards,
------
Sergei
More information about the Agda
mailing list