--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on June 2012 ---
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