Merge #11390: [docs] document scripted-diff

90ab62c [docs] document scripted-diff (John Newbery)

Pull request description:

  Document scripted-diffs in developer-notes.md

  I sometimes comment on PRs that a scripted-diff would be appropriate, but I don't have any documentation to point to. Fix that.

Tree-SHA512: 7d4a14b9217c812e4c27601e5e6dd8054cf5104cd20ecbe1ec0a84c217cc4b0645b7c0d2e3a89fdd4d059cafbc388acbddba75a430308f8279200b9383e009de

doc/developer-notes.md

@@ -549,6 +549,26 @@ Git and GitHub tips
   or `git fetch upstream-pull`. Afterwards, you can use `upstream-pull/NUMBER/head` in arguments to `git show`,
   `git checkout` and anywhere a commit id would be acceptable to see the changes from pull request NUMBER.
 
+Scripted diffs
+--------------
+
+For reformatting and refactoring commits where the changes can be easily automated using a bash script, we use
+scripted-diff commits. The bash script is included in the commit message and our Travis CI job checks that
+the result of the script is identical to the commit. This aids reviewers since they can verify that the script
+does exactly what it's supposed to do. It is also helpful for rebasing (since the same script can just be re-run
+on the new master commit).
+
+To create a scripted-diff:
+
+- start the commit message with `scripted-diff:` (and then a description of the diff on the same line)
+- in the commit message include the bash script between lines containing just the following text:
+    - `-BEGIN VERIFY SCRIPT-`
+    - `-END VERIFY SCRIPT-`
+
+The scripted-diff is verified by the tool `contrib/devtools/commit-script-check.sh`
+
+Commit `bb81e173` is an example of a scripted-diff.
+
 RPC interface guidelines
 --------------------------