From 53c86f202b3aad7d9b489734b6dcd340b7054ebb Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 21 Sep 2024 09:05:39 -0700 Subject: [PATCH] Fixes --- README.md | 2 ++ src/scripts/merge_tools/gitmerge.sh | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 5e1a3ba844..01415643a4 100644 --- a/README.md +++ b/README.md @@ -246,6 +246,8 @@ To investigate differences between two mergers: * Set `DELETE_WORKDIRS` to `false` in `src/python/variables.py`. * run `src/python/replay_merge.py --idx INDEX` (maybe add `-test`) for the index of the merge you are interested in. +If the merge is in the small test, you may need to add `--merges_csv ./test/small-goal-files/result.csv`. + ## Overwriting results manually In some cases it might be worth to overwrite the computed results. To do that you should modify the `results/manual_override.csv` file. In that file for the merge you want to overwrite a result of you should include at least the information `repository,merge,left,right` and a new column for the result you want to overwrite. You can overwrite anything you want but if there is a column you don't want to overwrite either do not include that column or leave the entry blanck i.e. `,,`. See the file for an example. diff --git a/src/scripts/merge_tools/gitmerge.sh b/src/scripts/merge_tools/gitmerge.sh index 934426faf7..04269a0fb9 100755 --- a/src/scripts/merge_tools/gitmerge.sh +++ b/src/scripts/merge_tools/gitmerge.sh @@ -1,6 +1,5 @@ #!/usr/bin/env sh -# usage: ./git_hires_merge_plus.sh # usage: ./gitmerge.sh # Merges branch2 into branch1, in , using merge strategy . # must contain a clone of a repository.