aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--test/monniaux/Makefile6
1 files changed, 4 insertions, 2 deletions
diff --git a/test/monniaux/Makefile b/test/monniaux/Makefile
index c864cf4e..12f2bfe2 100644
--- a/test/monniaux/Makefile
+++ b/test/monniaux/Makefile
@@ -6,14 +6,16 @@ CCOMP?=ccomp
all: measures.csv
verifier_times.txt: Asmblockdeps.patch
+ (cd ../../ && make -j20)
patch $(realpath ../../extraction/Asmblockdeps.ml) < $<
- (cd ../../ && make -j20 && make install); patch -R $(realpath ../../extraction/Asmblockdeps.ml) < $<
+ (cd ../../ && make -j20); patch -R $(realpath ../../extraction/Asmblockdeps.ml) < $<
bash clean_benches.sh
bash build_benches.sh $@
oracle_times.txt: PostpassSchedulingOracle.patch
+ (cd ../../ && make -j20)
patch $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
- (cd ../../ && make -j20 && make install); patch -R $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
+ (cd ../../ && make -j20); patch -R $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
bash clean_benches.sh
bash build_benches.sh $@