mirror of
https://github.com/enso-org/enso.git
synced 2024-12-24 10:02:17 +03:00
Action to update dev docs (https://github.com/enso-org/ide/pull/618)
Original commit: d4db47ca02
This commit is contained in:
parent
30d4cc7562
commit
ead7e32718
39
gui/.github/workflows/docs.yml
vendored
Normal file
39
gui/.github/workflows/docs.yml
vendored
Normal file
@ -0,0 +1,39 @@
|
||||
name: Publish Developer Docs
|
||||
|
||||
on:
|
||||
push:
|
||||
branches:
|
||||
- main
|
||||
paths:
|
||||
- 'docs/**'
|
||||
|
||||
jobs:
|
||||
checkout:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- uses: actions/checkout@v2
|
||||
with:
|
||||
repository: 'enso-org/enso-org.github.io'
|
||||
ref: 'sources'
|
||||
token: ${{ secrets.ENSO_PAT }}
|
||||
- name: set identity email
|
||||
run: git config --global user.email "actions@github.com"
|
||||
- name: set identity name
|
||||
run: git config --global user.name "GitHub Actions"
|
||||
- name: Checkout submodules
|
||||
run: git submodule update --init
|
||||
- name: Update submodules
|
||||
id: status
|
||||
run: |
|
||||
git submodule update --init
|
||||
git submodule update --remote --merge
|
||||
if [ -n "$(git status --porcelain)" ]; then
|
||||
echo "::set-output name=has_changes::1"
|
||||
fi
|
||||
- name: Push changes
|
||||
run: |
|
||||
git add .
|
||||
git commit -m "Update submodules"
|
||||
git push origin sources
|
||||
if: steps.status.outputs.has_changes == '1'
|
||||
|
Loading…
Reference in New Issue
Block a user