--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on June 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with ptests



On Fri, 2012-06-22 at 17:36 +0200, Virgile Prevosto wrote:
> Did you launch the tests with make tests or directly with ptests.byte?
> In the latter case, you might need to generate ptests_local_config.cmo
> in the main directory of your plug-in
> (if you have a Makefile that includes Makefile.dynamic, simply make
> ptests_local_config.cmo. make tests does that implicitly, so that you
> don't need this step).

thanks, this solved the problem. Now I've moved all my tests to ./tests
and I use make tests.
-- 
Best regards,
Boris