diff options
| author | Alexandre Flament <alex@al-f.net> | 2021-02-02 08:37:00 +0100 |
|---|---|---|
| committer | Alexandre Flament <alex@al-f.net> | 2021-02-02 08:53:57 +0100 |
| commit | 90b9d0d6a8248832ba5a093ba7540ea6dd9b531a (patch) | |
| tree | 2153107cc67d0237fb21df1e1116c635eaf68c3b | |
| parent | 34de715e620a192185e093e1e6caca04ae3cb77a (diff) | |
[mod] CI: minor changes
* utils/makefile.python: travis-gh-pages renamed ci-gh-pages
| -rw-r--r-- | .github/workflows/integration.yml | 2 | ||||
| -rw-r--r-- | utils/makefile.sphinx | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/.github/workflows/integration.yml b/.github/workflows/integration.yml index 7d0b9744..59eb4c56 100644 --- a/.github/workflows/integration.yml +++ b/.github/workflows/integration.yml @@ -73,7 +73,7 @@ jobs: python-version: '3.9' architecture: 'x64' - name: Build documentation - run: SEARX_DEBUG=1 make V=1 travis-gh-pages + run: SEARX_DEBUG=1 make V=1 ci-gh-pages - name: Deploy if: github.ref == 'refs/heads/master' uses: JamesIves/github-pages-deploy-action@3.7.1 diff --git a/utils/makefile.sphinx b/utils/makefile.sphinx index c0f39e87..b674cf7f 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 |