Skip to content
Snippets Groups Projects
Commit 56dbfbfb authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[ci] do not use --root for ptests

parent 1b819b90
No related branches found
No related tags found
No related merge requests found
......@@ -89,6 +89,8 @@ stdenv.mkDerivation rec {
buildPhase = ''
make config.sed
dune build -j2 --display short @install
make ptests/ptests.exe
make ptests/wtests.exe
'';
installFlags = [
......
......@@ -32,9 +32,7 @@ stdenv.mkDerivation rec {
'';
buildPhase = ''
make ptests/ptests.exe
make ptests/wtests.exe
dune exec --root ptests -- frama-c-ptests tests
dune exec -- frama-c-ptests tests
dune build -j1 --display short @tests/ptests
'';
......
......@@ -40,9 +40,7 @@ stdenv.mkDerivation rec {
buildPhase = ''
export FRAMAC_WP_CACHEDIR=$wp_cache
make ptests/ptests.exe
make ptests/wtests.exe
dune exec --root ptests -- frama-c-ptests src/plugins/*/tests
dune exec -- frama-c-ptests src/plugins/*/tests
dune build -j1 --display short @src/plugins/ptests
'';
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment