From e8c7a6d6f2317bc1feecc984ae78da300805c8d9 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 10 May 2024 10:21:46 -0700 Subject: [PATCH] Update mergers --- README.md | 2 +- src/scripts/merge_tools/merging | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index b3dec663f1..80c0ff763d 100644 --- 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 index 96a0837010..9abe781d0d 160000 --- a/src/scripts/merge_tools/merging +++ b/src/scripts/merge_tools/merging @@ -1 +1 @@ -Subproject commit 96a08370101833c4205dbe8fde48214c0a381c1e +Subproject commit 9abe781d0d6604e020dffd8f958c9344c2ab9b30