Merge branch 'main' into trivial_merges

benedikt-schesch · Oct 18, 2023 · c9e796d · c9e796d
2 parents c108229 + 1d71aa6
commit c9e796d
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/run_1000.sh b/run_1000.sh
@@ -18,4 +18,5 @@ if [ -f cache.tar ] && [ ! -d cache ]; then
     make decompress-cache
 fi
 
-./run.sh input_data/repos_1000.csv results_trivial_merges 20 cache "$@"
+
+./run.sh input_data/repos_1000.csv results-trivial-merges 20 cache "$@"