aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-26 15:55:46 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-05 13:05:49 +0200
commit274da8930804b2187568423c3bfeed541f235001 (patch)
tree01af560021c849131e0aa25afbfb1a2e504636df /dev/doc
parent19bbdb467360578c98d9787a9aebca4bf246a8e9 (diff)
Some advice about merge script dependencies.
Including: how to create a GPG key.
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/MERGING.md11
1 files changed, 11 insertions, 0 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 70d848188..402ed37bd 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -104,3 +104,14 @@ There are two cases to consider:
merge the PR and then notify upstream they can merge the patch. This is a
less preferable scenario because it is probably going to create
spurious CI failures for unrelated PRs.
+
+### Merge script dependencies
+
+The merge script passes option `-S` to `git merge` to ensure merge commits
+are signed. Consequently, it depends on the GnuPG command utility being
+installed and a GPG key being available. Here is a short tutorial to
+creating your own GPG key:
+<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/>
+
+The script depends on a few other utilities. If you are a Nix user, the
+simplest way of getting them is to run `nix-shell` first.