Skip to content

Fix stepper pointer events #4998

Fix stepper pointer events

Fix stepper pointer events #4998

# General notes on github actions: Note that both the working directory
# and environment variables generally are not shared between steps.
name: Build and Deploy Hazel
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 the hazel repo on the current branch
uses: actions/checkout@v2
with:
path: source
- name: Add the name of the current branch to the environment as BRANCH_NAME
uses: nelonoel/[email protected]
- name: Retrieve the build environment if cached
id: opam-cache
uses: actions/cache@v2
with:
path: '/home/runner/.opam/'
key: ${{ runner.os }}-modules-${{ hashFiles('./source/opam.export') }}
- name: Set-up OCaml
run: |
sudo apt --assume-yes install curl m4 opam
export OPAMYES=1
opam init --compiler=ocaml-base-compiler.5.0.0
- name: Install dependencies
run: |
eval $(opam env)
export OPAMYES=1
make deps
working-directory: ./source
- name: Build Hazel
run: |
eval $(opam env)
make release
working-directory: ./source
- name: Run Tests
id: test
continue-on-error: true
run: |
eval $(opam env)
make test > test_output
if [ $? -eq 0 ]; then
echo "::set-output name=tests_passed::true"
else
echo "::set-output name=tests_passed::false"
fi
working-directory: ./source
- name: Test Report
uses: dorny/test-reporter@v1
continue-on-error: true
with:
name: Test Report
path: junit_tests*.xml
reporter: java-junit
fail-on-error: true
working-directory: ./source
- name: Checkout the website build artifacts repo
uses: actions/checkout@v2
with:
repository: hazelgrove/build
token: ${{ secrets.ACCESS_TOKEN }}
path: server
- name: Clear any old build of this branch
run: if [ -d "${BRANCH_NAME}" ] ; then rm -rf "${BRANCH_NAME}" ; fi
working-directory: ./server
- name: Copy in the newly built source
run: mkdir "./server/${BRANCH_NAME}" && cp -r "./source/_build/default/src/haz3lweb/www"/* "./server/${BRANCH_NAME}"
- name : Commit to the website aka deploy
run: |
git config user.name github-deploy-action
git config user.email [email protected]
git add -A
git pull --no-edit
git status
git diff-index --quiet HEAD || (git commit -m "github-deploy-action-${BRANCH_NAME}"; git push)
working-directory: ./server