[ fix ] include text layout instructions when measuring metrics #440
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
--- | |
name: Build | |
on: | |
push: | |
branches: | |
- '**' | |
tags: | |
- '**' | |
pull_request: | |
branches: | |
- main | |
schedule: | |
- cron: '0 1 * * *' | |
defaults: | |
run: | |
shell: bash | |
jobs: | |
build: | |
name: Build ${{ github.repository }} with Idris2 latest | |
runs-on: ubuntu-latest | |
env: | |
PACK_DIR: /root/.pack | |
strategy: | |
fail-fast: false | |
container: ghcr.io/stefan-hoeck/idris2-pack:latest | |
steps: | |
- name: Checkout | |
uses: actions/checkout@v2 | |
- name: Build library | |
run: pack install dom-mvc | |
- name: Check docs | |
run: pack typecheck dom-mvc-docs | |
- name: Check extra | |
run: pack typecheck dom-mvc-extra |