use merge queue

This commit is contained in:
MarcoIeni 2024-11-27 09:55:29 +01:00 committed by Amanieu d'Antras
parent ecf58b32ff
commit 60249f87f6
2 changed files with 26 additions and 14 deletions

View file

@ -0,0 +1,25 @@
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

View file

@ -1,12 +1,7 @@
name: CI
on:
push:
branches:
- auto
- try
pull_request:
branches:
- master
merge_group:
jobs:
style:
@ -29,14 +24,6 @@ jobs:
- 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
if: github.event_name == 'push' && github.event.ref == 'refs/heads/master'
verify:
name: Automatic intrinsic verification