From a8cfc0cc2c7b913649dfa4e98814cfedd9dc3e97 Mon Sep 17 00:00:00 2001 From: Victor Zverovich Date: Sun, 9 Jun 2024 16:34:50 -0700 Subject: [PATCH] Deploy dev docs --- .github/workflows/doc.yml | 3 +-- support/mkdocs | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index 4ac8930f..06705bcb 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -34,5 +34,4 @@ jobs: KEY: ${{secrets.KEY}} run: | cmake $GITHUB_WORKSPACE - make doc - # $GITHUB_WORKSPACE/support/build-docs.py + $GITHUB_WORKSPACE/support/mkdocs deploy dev -p diff --git a/support/mkdocs b/support/mkdocs index d18302f3..746aaf32 100755 --- a/support/mkdocs +++ b/support/mkdocs @@ -1,7 +1,7 @@ #!/usr/bin/env python3 # A script to invoke mkdocs with the correct environment. -# Additionally supports deploying: -# ./mkdocs deploy ... +# Additionally supports deploying via mike: +# ./mkdocs deploy [mike-deploy-options] import errno, os, shutil, sys from subprocess import call