Mirror master and main

In preparation for eventually switching over to `main`, let's
synchronize the historical and the designated future main branch.

This follows the excellent advice from
https://github.com/chancancode/branch-rename/#gradual-migration

Signed-off-by: Johannes Schindelin <johannes.schindelin@gmx.de>

Author: dscho

.github/workflows/mirror-master-and-main.yml

@@ -0,0 +1,17 @@
+name: Mirror "master" and "main" branches
+on:
+  push:
+    branches:
+      - master
+      - main
+
+jobs:
+  mirror:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Partial clone
+        run: git clone --bare --depth=100 --single-branch --filter=blob:none ${{ github.event.repository.html_url }} .
+      - name: Push
+        run: |
+          git config http.https://github.com/.extraheader "Authorization: Basic $(echo -n x-access-token:${{ github.token }} | base64 --wrap=0)"
+          git push origin HEAD:master HEAD:main