about summary refs log tree commit diff
path: root/library/stdarch/.github/workflows
diff options
context:
space:
mode:
authorMarcoIeni <11428655+MarcoIeni@users.noreply.github.com>2024-11-27 09:55:29 +0100
committerAmanieu d'Antras <amanieu@gmail.com>2024-11-28 15:24:24 +0000
commit60249f87f6ff57d96d97e1c8c8566fc0d2174d62 (patch)
tree4a19214fcf438c5cd760527910902ab5e2d794c0 /library/stdarch/.github/workflows
parentecf58b32ff82eade5b60c1a8cb2e0ac5386764ca (diff)
use merge queue
Diffstat (limited to 'library/stdarch/.github/workflows')
-rw-r--r--library/stdarch/.github/workflows/doc.yml25
-rw-r--r--library/stdarch/.github/workflows/main.yml15
2 files changed, 26 insertions, 14 deletions
diff --git a/library/stdarch/.github/workflows/doc.yml b/library/stdarch/.github/workflows/doc.yml
new file mode 100644
index 00000000000..d2887b369a3
--- /dev/null
+++ b/library/stdarch/.github/workflows/doc.yml
@@ -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
diff --git a/library/stdarch/.github/workflows/main.yml b/library/stdarch/.github/workflows/main.yml
index 6fa886f15c9..6701cf52f03 100644
--- a/library/stdarch/.github/workflows/main.yml
+++ b/library/stdarch/.github/workflows/main.yml
@@ -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