Add fuzz-corpora to review-tools

[tools.git] / review-tools / ghmerge

diff --git a/review-tools/ghmerge b/review-tools/ghmerge
index 7a8fae15470c80972d68359365d7f32bc8d06580..41e3faefd6a350972ce8a86bc1ff3171ca52f331 100755 (executable)
--- a/review-tools/ghmerge
+++ b/review-tools/ghmerge
@@ -10,6 +10,7 @@ Option style arguments:
 --help              Print this help and exit
 --tools             Merge a tools PR (rather than openssl PR)
 --web               Merge a web PR (rather than openssl PR)
+--fuzz-corpora      Merge a PR against fuzz-corpora (rather than openssl PR)
 --remote <remote>   Repo to merge with (rather than git.openssl.org), usually 'upstream'
 --target <branch>   Merge target (rather than current branch), usually 'master'
 --ref <branch>      A synonym for --target
@@ -60,6 +61,9 @@ while [ $# -ne 0 ]; do
     --web)
         WHAT=web ; BUILD=no ; shift
         ;;
+    --fuzz-corpora)
+        WHAT=fuzz-corpora ; BUILD=no ; shift
+        ;;
     --cherry-pick)
         shift;
         PICK=1;