fast-forward: Add --no-ff merge support

This change allows to choose the merge strategy to use for merging
the pull-request.

A merge-strategy parameter is added, allowing to choose the no-ff way
(i.e. introducing a merge commit). The default strategy remains
fast-forwarding the branch.

Fixes sequoia-pgp#36

action.yml

@@ -15,6 +15,14 @@ inputs:
       indicating whether it is possible to fast forward the target
       branch.
     default: false
+  merge-method:
+    description: >
+      When merging, whether fast forwarding the branch or creating a
+      merge commit.
+
+      If merge-commit, a merge commit is created. Otherwise (the default),
+      the branch is fast forwarded.
+    default: fast-forward
   comment:
     description: >
       Whether to post a comment.
@@ -61,7 +69,13 @@ runs:
         # github.action_path is set to $REPO.
         if test "x${{ inputs.merge }}" = xtrue
         then
-            ${{ github.action_path }}/src/fast-forward.sh --merge
+            if test "x${{ inputs.merge-method }}" = xmerge-commit
+            then
+                MERGE_METHOD=merge-commit
+            else
+                MERGE_METHOD=fast-forward
+            fi
+            ${{ github.action_path }}/src/fast-forward.sh --merge "${MERGE_METHOD}"
         else
             ${{ github.action_path }}/src/fast-forward.sh
         fi

src/fast-forward.sh

@@ -286,17 +286,36 @@ LOG=$(mktemp)
 
         if test "x$(jq -r .user.permissions.push < $PERM)" = xtrue
         then
-            echo -n "Fast forwarding \`$BASE_REF\` ($BASE_SHA) to"
-            echo " \`$PR_REF\` ($PR_SHA)."
+            if test "x$2" = "xmerge-commit"
+            then
+                echo -n "Merging \`$PR_REF\` ($PR_SHA) into \`$BASE_REF\` ($BASE_SHA)."
+
+                echo '```shell'
+                (
+                    PS4='$ '
+                    set -x
+                    git checkout "${BASE_REF}"
+                    git merge --no-ff --into-name "${BASE_REF}" \
+                        -m "Merge pull request $(github_pull_request .number) from ${PR_REF} into ${BASE_REF}" \
+                        "${PR_SHA}"
+                    git push origin "${BASE_REF}"
+                )
+                echo '```'
+                echo 0 >$EXIT_CODE
 
-            echo '```shell'
-            (
-                PS4='$ '
-                set -x
-                git push origin "$PR_SHA:$BASE_REF"
-            )
-            echo '```'
-            echo 0 >$EXIT_CODE
+            else
+                echo -n "Fast forwarding \`$BASE_REF\` ($BASE_SHA) to"
+                echo " \`$PR_REF\` ($PR_SHA)."
+
+                echo '```shell'
+                (
+                    PS4='$ '
+                    set -x
+                    git push origin "$PR_SHA:$BASE_REF"
+                )
+                echo '```'
+                echo 0 >$EXIT_CODE
+            fi
         else
             echo -n "Sorry @$(github_event .sender.login),"
             echo -n " it is possible to fast forward \`$BASE_REF\` ($BASE_SHA)"