Skip to content

Commit 1fd5f09

Browse files
committed
CI: update publication flow.
1 parent c169583 commit 1fd5f09

File tree

1 file changed

+3
-22
lines changed

1 file changed

+3
-22
lines changed

.github/workflows/main.yaml

Lines changed: 3 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
on:
22
push:
33
pull_request:
4+
workflow_dispatch:
45

56
name: CI
67
jobs:
@@ -20,28 +21,7 @@ jobs:
2021
name: dist
2122
path: dist/
2223

23-
deploy:
24-
needs: build
25-
if: ${{ github.repository == 'amaranth-lang/playground' && github.event_name == 'push' && github.event.ref == 'refs/heads/live' }}
26-
runs-on: ubuntu-latest
27-
steps:
28-
- name: Check out repository
29-
uses: actions/checkout@v4
30-
- name: Download artifact
31-
uses: actions/download-artifact@v4
32-
with:
33-
name: dist
34-
path: dist/
35-
- name: Publish artifact to the main Amaranth website
36-
uses: JamesIves/github-pages-deploy-action@releases/v4
37-
with:
38-
folder: dist/
39-
repository-name: amaranth-lang/amaranth-lang.github.io
40-
ssh-key: ${{ secrets.PAGES_DEPLOY_KEY }}
41-
branch: main
42-
target-folder: play/
43-
44-
deploy-dev:
24+
publish:
4525
needs: build
4626
if: ${{ github.event_name == 'push' && github.event.ref == 'refs/heads/main' }}
4727
runs-on: ubuntu-latest
@@ -62,4 +42,5 @@ jobs:
6242
uses: JamesIves/github-pages-deploy-action@releases/v4
6343
with:
6444
folder: dist/
45+
branch: ${{ github.repository == 'amaranth-lang/playground' && 'pages' || 'gh-pages' }}
6546
single-commit: true

0 commit comments

Comments
 (0)