diff options
| author | Alexandre Flament <alex@al-f.net> | 2021-02-04 23:12:27 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-04 23:12:27 +0100 |
| commit | 321788f14a8a674984b9884094dd9626d6162a33 (patch) | |
| tree | db50773e7601bd1ff02dcc113b1b6d0e868ea659 /utils/makefile.sphinx | |
| parent | ffaf785f8272a8168e92dfe1c3a2179b6991bb18 (diff) | |
| parent | 90b9d0d6a8248832ba5a093ba7540ea6dd9b531a (diff) | |
Merge pull request #2528 from dalf/mod-ci-gh-pages
[mod] CI: minor changes
Diffstat (limited to 'utils/makefile.sphinx')
| -rw-r--r-- | utils/makefile.sphinx | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/utils/makefile.sphinx b/utils/makefile.sphinx index c0f39e87d..b674cf7f0 100644 --- a/utils/makefile.sphinx +++ b/utils/makefile.sphinx @@ -186,8 +186,8 @@ gh-pages: docs-clean docs git commit -q -m "make gh-pages: from $(shell git config --get remote.origin.url)@$(shell git rev-parse HEAD)" ;\ git push -f origin gh-pages -PHONY += travis-gh-pages -travis-gh-pages: docs-clean docs +PHONY += ci-gh-pages +ci-gh-pages: docs-clean docs rm -Rf $(GH_PAGES) mkdir -p $(GH_PAGES) $(MAKE) prepare-gh-pages |