Instructions for adding a new merge tool

benedikt-schesch · Nov 14, 2024 · cda753d · cda753d
1 parent 331aba2
commit cda753d
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/src/scripts/merge_tools/README b/src/scripts/merge_tools/README
@@ -1 +1,7 @@
-git-hires-merge is from https://github.com/paulaltin/git-hires-merge .
+To add a new merging tool to the evaluation:
+ * Add a new script here, `mytool.sh`
+ * Create a `mytool_plus.sh` script that runs the new merging tool and then
+   Plume-lib Merging.  (You can copy from `spork_plus.sh`.)
+ * Update the expected results so that the CI tests pass.
+
+File `git-hires-merge` is from https://github.com/paulaltin/git-hires-merge .