add gh workflow which will delete docs in mike when a reference is de…

…leted (#322)

.github/workflows/clean-docs.yml

@@ -0,0 +1,33 @@
+name: Clean Docs for Deleted References
+on:
+  delete:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        python-version: [3.8]
+
+    steps:
+    - uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Document branch deleting
+      run: echo ${{ github.ref_name }}
+    - name: Set up Python ${{ matrix.python-version }}
+      uses: actions/setup-python@v2
+      with:
+        python-version: ${{ matrix.python-version }}
+    - name: Install mike
+      run: |
+        python -m pip install --upgrade pip
+        pip install mike
+    - name: Configure Git user
+      run: |
+        git config --local user.email "github-actions[bot]@users.noreply.github.com"
+        git config --local user.name "github-actions[bot]"
+    - name: Delete defunct docs versions
+      run: |
+        echo "Deleting ${{ github.event.ref_name }} version from docs"
+        mike delete --rebase --push ${{ github.event.ref_name }}