Deploy dev docs

This commit is contained in:
Victor Zverovich 2024-06-09 16:34:50 -07:00
parent 65e278b286
commit a8cfc0cc2c
2 changed files with 3 additions and 4 deletions

View File

@ -34,5 +34,4 @@ jobs:
KEY: ${{secrets.KEY}} KEY: ${{secrets.KEY}}
run: | run: |
cmake $GITHUB_WORKSPACE cmake $GITHUB_WORKSPACE
make doc $GITHUB_WORKSPACE/support/mkdocs deploy dev -p
# $GITHUB_WORKSPACE/support/build-docs.py

View File

@ -1,7 +1,7 @@
#!/usr/bin/env python3 #!/usr/bin/env python3
# A script to invoke mkdocs with the correct environment. # A script to invoke mkdocs with the correct environment.
# Additionally supports deploying: # Additionally supports deploying via mike:
# ./mkdocs deploy ... # ./mkdocs deploy [mike-deploy-options]
import errno, os, shutil, sys import errno, os, shutil, sys
from subprocess import call from subprocess import call