Skip to content

Commit

Permalink
Update CI for Lean-zh
Browse files Browse the repository at this point in the history
  • Loading branch information
OlingCat committed Jun 2, 2024
1 parent 81b0283 commit d4d163a
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 50 deletions.
64 changes: 32 additions & 32 deletions .github/workflows/deploy.yml
Original file line number Diff line number Diff line change
@@ -1,32 +1,32 @@
name: mdbook deploy to github pages

on:
push:
branches:
- master

jobs:
Build:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
- name: Download mdbook for Lean
shell: bash
run: |
curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.6/mdbook-linux.tar.gz
tar xvf mdbook-linux.tar.gz
./mdbook-linux/mdbook --help
ldd ./mdbook-linux/mdbook
- name: Run mdbook build
shell: bash
run: |
./mdbook-linux/mdbook build
rm -rf ./out/.git
rm -rf ./out/.github
- name: Deploy 🚀
uses: JamesIves/[email protected]
with:
branch: gh-pages
folder: out

name: mdbook deploy to github pages

on:
push:
branches:
- master

jobs:
Build:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
- name: Download mdbook for Lean
shell: bash
run: |
curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.6/mdbook-linux.tar.gz
tar xvf mdbook-linux.tar.gz
./mdbook-linux/mdbook --help
ldd ./mdbook-linux/mdbook
- name: Run mdbook build
shell: bash
run: |
./mdbook-linux/mdbook build
rm -rf ./out/.git
rm -rf ./out/.github
- name: Deploy 🚀
uses: JamesIves/[email protected]
with:
branch: gh-pages
folder: out

36 changes: 18 additions & 18 deletions deploy.sh
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
#!/usr/bin/env bash
set -e

# Build
mdbook build
rm -rf out/.git

# 3. Deploy
rm -rf deploy
mkdir deploy
cd deploy
git init
cp -r ../out/./ .
git add -A
git commit -m "Update `date`"
git push https://github.com/leanprover/theorem_proving_in_lean4.git +HEAD:gh-pages
cd ..
rm -rf deploy
#!/usr/bin/env bash
set -e

# Build
mdbook build
rm -rf out/.git

# 3. Deploy
rm -rf deploy
mkdir deploy
cd deploy
git init
cp -r ../out/./ .
git add -A
git commit -m "Update `date`"
git push https://github.com/Lean-zh/tp-lean-zh.git +HEAD:gh-pages
cd ..
rm -rf deploy

0 comments on commit d4d163a

Please sign in to comment.