Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions .github/workflows/unversioned_pages.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
name: Copy unversioned pages

on:
push:
branches:
- gh-pages
paths:
- 'dev/developers/**'
- 'dev/index.html'
workflow_dispatch:

jobs:
copy-pages:
name: Copy unversioned pages
runs-on: ubuntu-latest
steps:
- name: Clone artifacts repo
uses: actions/checkout@v4

- name: Copy pages
run: |
ls -la
cp -Rv ./dev/developers/ ./stable/
cp -v ./dev/index.html ./stable/
Comment on lines +22 to +24
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this really a good idea? Once we updated theme, the copied pages will be with new theme, when rest will be with old one.
I think that we should use same approach as in banner. So we should have JS that will download page from dev, extract content from dev and then replace current with one from dev.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you mean: a javascript that, every time the developer docs are accessed by a reader, replaces the contents on the fly? I have not explored this possibility, I can take a look 🤔


- name: Commit files
run: |
git config --local user.email "action@github.com"
git config --local user.name "GitHub Action"
git commit -m "Copy unversioned files" -a

- name: Push changes
uses: ad-m/github-push-action@master
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
branch: gh-pages