From b9539a36e74ab40bd00da6536b34127013c1b24d Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 1 Sep 2024 17:41:16 -0700 Subject: [PATCH] Documentation tweaks --- src/scripts/merge_tools/gitmerge.sh | 3 ++- src/scripts/merge_tools/merge_plumelib.sh | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/scripts/merge_tools/gitmerge.sh b/src/scripts/merge_tools/gitmerge.sh index 0fdbeddd10..abcef148da 100755 --- a/src/scripts/merge_tools/gitmerge.sh +++ b/src/scripts/merge_tools/gitmerge.sh @@ -19,7 +19,8 @@ branch1=$2 branch2=$3 strategy=$4 -# perform merge +## Perform merge + cd "$clone_dir" || (echo "$0: cannot cd to $clone_dir" ; exit 1) git checkout "$branch1" --force diff --git a/src/scripts/merge_tools/merge_plumelib.sh b/src/scripts/merge_tools/merge_plumelib.sh index ebfe4745a0..24dcebd971 100755 --- a/src/scripts/merge_tools/merge_plumelib.sh +++ b/src/scripts/merge_tools/merge_plumelib.sh @@ -8,6 +8,8 @@ branch2=$3 git_strategy=$4 #"-Xignore-space-change" merge_strategy=$5 #"--only-adjacent" +## Perform merge + echo "$0: Merging $branch1 and $branch2 with git_strategy=$git_strategy and merge_strategy=$merge_strategy" cd "$clone_dir" || (echo "$0: cannot cd to $clone_dir" ; exit 1) @@ -24,6 +26,8 @@ git config --local mergetool.merge-plumelib.trustExitCode true # shellcheck disable=SC2086 git merge --no-edit $git_strategy "$branch2" +## Now, run Plume-lib Merging to improve the result of `git merge`. + case "$merge_strategy" in *"--no-imports"* | *"--only-adjacent"* | *"--only-annotations"* | *"--only-version-numbers"*) # The "imports" merger is not being used, so don't use the "--all" command-line option.