summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.github/workflows/integration.yml2
-rw-r--r--utils/makefile.sphinx4
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