diff options
Diffstat (limited to '.github/workflows/gh-pages.yml')
-rw-r--r-- | .github/workflows/gh-pages.yml | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml deleted file mode 100644 index ed7e032..0000000 --- a/.github/workflows/gh-pages.yml +++ /dev/null @@ -1,29 +0,0 @@ -name: docs - -on: - push: - branches: [ master ] - pull_request: - branches: [ master ] - -jobs: - build: - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v2 - - - name: Install emacs - run: sudo apt-get install emacs - - - name: Generate documentation - run: cd docs && emacs --batch --no-init --load publish.el --funcall org-publish-all - - - name: Generate Admitted icon - run: python3 scripts/statistics.py src && mkdir -p docs/html/assets && mv admitted.svg docs/html/assets/. - - - name: Deploy gh-pages - uses: peaceiris/actions-gh-pages@v3 - with: - github_token: ${{ secrets.GITHUB_TOKEN }} - publish_dir: ./docs/html |