[mod] CI: minor changes

* utils/makefile.python: travis-gh-pages renamed ci-gh-pages

.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

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