From c5e55972aeee5703dd351ccd4941bf559e2eee9b Mon Sep 17 00:00:00 2001 From: Victor Zverovich Date: Sun, 21 Sep 2025 12:46:52 -0700 Subject: [PATCH] Minor improvements to mkdocs --- support/mkdocs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/support/mkdocs b/support/mkdocs index aa8666b5..94eddae3 100755 --- a/support/mkdocs +++ b/support/mkdocs @@ -4,7 +4,8 @@ # ./mkdocs deploy [mike-deploy-options] # For example: # ./mkdocs deploy -# This will checkout website to fmt/build/fmt.dev and deploy to it. +# This will checkout the website to fmt/build/fmt.dev and deploy documentation +# there. import errno, os, shutil, sys from subprocess import call @@ -43,7 +44,7 @@ config_path = os.path.join(support_dir, 'mkdocs.yml') args = sys.argv[1:] if len(args) > 0: command = args[0] - if command == 'deploy': + if command == 'deploy' or command == 'set-default': git_url = 'https://github.com/' if 'CI' in os.environ else 'git@github.com:' site_repo = git_url + 'fmtlib/fmt.dev.git'