1 files changed, 3 insertions, 0 deletions

diff --git a/run_all_dis.sh b/run_all_dis.sh
index 588538d..3907789 100755
--- a/run_all_dis.sh
+++ b/run_all_dis.sh
@@ -16,6 +16,9 @@ if [[ "$EUID" != 0 ]]; then
 fi
 date
 
+# Configure libextra for benchmarking
+sed -i "s/LITMUS 1/LITMUS 0/g" extra.h
+
 # Run the pairs baseline and some comparisons to examine the effect of less cache
 echo "Building benchmarks in unpaired configuration..."
 cd dis