remove docs publishing

This commit is contained in:
MarcoIeni
2024-11-27 16:17:46 +01:00
committed by Amanieu d'Antras
parent 5f434100eb
commit f1cadfda0c
-25
View File
@@ -1,25 +0,0 @@
name: Docs
on:
push:
branches:
- master
jobs:
docs:
name: Publish Documentation
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install Rust
run: rustup update nightly --no-self-update && rustup default nightly
- run: ci/dox.sh
env:
CI: 1
- name: Publish documentation
run: |
cd target/doc
git init
git add .
git -c user.name='ci' -c user.email='ci' commit -m init
git push -f -q https://git:${{ secrets.github_token }}@github.com/${{ github.repository }} HEAD:gh-pages