Attempt to fix docs

Cribbed from https://cloudblogs.microsoft.com/opensource/2019/04/05/publishing-github-pages-from-azure-pipelines/
and https://docs.microsoft.com/en-us/azure/devops/pipelines/tasks/utility/install-ssh-key?view=azure-devops

azure-pipelines.yml

@@ -1,5 +1,4 @@
 jobs:
-
   - job: check_formatting
     displayName: Check formatting
     pool:
@@ -35,11 +34,11 @@ jobs:
     variables:
       - group: github-keys
     steps:
-    # - task: InstallSSHKey@0
-    #   inputs:
-    #     hostName: $(secret.GHSshKnownHosts)
-    #     sshPublicKey: $(secret.GHSshPub)
-    #     sshKeySecureFile: $(secret.GHSshPriv)
+      - task: InstallSSHKey@0
+        inputs:
+          hostName: $(GHSshKnownHosts)
+          sshPublicKey: $(GHSshPub)
+          sshKeySecureFile: $(GHSshPriv)
       - script: |
           ./docs/book/ci-build.sh master
 

docs/book/ci-build.sh

@@ -44,6 +44,8 @@ git clean -fd
 git checkout gh-pages
 rm -rf $VERSION
 mv /tmp/book-content ./$VERSION
+git config --local user.name "Juniper Doc Bot"
+git config --local user.email "juniper@example.com"
 git add -A $VERSION
-git commit -m "Updated book for $VERSION"
+git commit -m "Updated book for $VERSION ***NO_CI***"
 git push origin gh-pages