From cda753d5d11a7643aa3f59b4df4a796bdb59a86d Mon Sep 17 00:00:00 2001
From: Michael Ernst <mernst@cs.washington.edu>
Date: Thu, 14 Nov 2024 08:57:30 -0800
Subject: [PATCH] Instructions for adding a new merge tool

---
 src/scripts/merge_tools/README | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/scripts/merge_tools/README b/src/scripts/merge_tools/README
index 228bc7b0bb..412bc16d24 100644
--- 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 .