Update mergers

benedikt-schesch · May 10, 2024 · e8c7a6d · e8c7a6d
1 parent ddd2148
commit e8c7a6d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -216,4 +216,4 @@ To run style checking run `make style`.
 
 To investigate differences between two mergers:
  * run `src/python/select_from_results.py` to produce a CSV file containing only the differences you are interested in.  See its [documentation (at top of file)](src/python/select_from_results.py) for how to run it.
- * run `src/python/replay_merge.py --merges_csv CSV_FILE --idx INDEX` (maybe add `-test`) for the index of the merge you are interested in.
+ * run `src/python/replay_merge.py --idx INDEX` (maybe add `-test`) for the index of the merge you are interested in.
diff --git a/src/scripts/merge_tools/merging b/src/scripts/merge_tools/merging