Skip to content

restore different-row bidelimited child borders #562

restore different-row bidelimited child borders

restore different-row bidelimited child borders #562

# General notes on github actions: Note that both the working directory
# and environment variables generally are not shared between steps.
name: deploy tylr
on: [push]
jobs:
Deploy:
runs-on: ubuntu-latest
steps:
# NOTE: position the below lines in the code between two steps
# and uncomment them to open an ssh connection at that point:
#- name: Debugging with ssh
# uses: lhotari/action-upterm@v1
- name: Checkout tylr repo on current branch # STEP 1
uses: actions/checkout@v2
with:
path: source
- name: Add name of current branch to environment as BRANCH_NAME
uses: nelonoel/branch-name@v1.0.1
- name: Retrieve build environment if cached # STEP 2
id: opam-cache
uses: actions/cache@v2
with:
path: '/home/runner/.opam/'
key: ${{ runner.os }}-modules-${{ hashFiles('./source/opam.export') }}
- name: Install dependencies and build tylr # STEP 3
run: |
sudo apt --assume-yes install opam
export OPAMYES=1
opam init --compiler=ocaml-base-compiler.5.0.0
eval $(opam env)
make deps
make release
working-directory: ./source
- name: Checkout website build artifacts repo # STEP 4
uses: actions/checkout@v2
with:
repository: hazelgrove/tylr-build
token: ${{ secrets.DEPLOY_TYLR }}
path: server
- name: Clear any old build of this branch # STEP 5
run: if [ -d "${BRANCH_NAME}" ] ; then rm -rf "${BRANCH_NAME}" ; fi
working-directory: ./server
- name: Copy in newly built source # STEP 6
run: |
mkdir "./server/${BRANCH_NAME}" &&
cp -r "./source/_build/default/src/web/www"/* "./server/${BRANCH_NAME}" &&
if [ "${BRANCH_NAME}" == "plus" ]
then
cp -r "./source/_build/default/src/web/www"/* "./server"
fi
- name: Commit to website aka deploy # STEP 7
run: |
git config user.name github-deploy-action
git config user.email tylr-deploy@hazel.org
git add -A
git status
git diff-index --quiet HEAD || (git commit -m "github-deploy-action-${BRANCH_NAME}"; git push)
working-directory: ./server