From 175004360d80753b131a18ab8602b1a0f80457bd Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 14 Aug 2020 00:06:03 +0100 Subject: Update workflow --- .github/workflows/main.yml | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) (limited to '.github/workflows/main.yml') diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 0c9391b..44309a2 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -1,25 +1,24 @@ -# This is a basic workflow to help you get started with Actions - name: CI -# Controls when the action will run. Triggers the workflow on push or pull request -# events but only for the master branch on: push: branches: [ master ] + paths: + - '**.v' + - '**.ml' + - '**.mli' pull_request: branches: [ master ] + paths: + - '**.v' + - '**.ml' + - '**.mli' -# A workflow run is made up of one or more jobs that can run sequentially or in parallel jobs: - # This workflow contains a single job called "build" build: - # The type of runner that the job will run on runs-on: ubuntu-latest - # Steps represent a sequence of tasks that will be executed as part of the job steps: - # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it - uses: actions/checkout@v2 with: submodules: true @@ -29,3 +28,11 @@ jobs: - name: Build run: nix-shell --run "make -j8" + + - name: Generate Documentation + run: nix-shell --run "make -j8 doc" + + - uses: actions/upload-artifact@v2 + with: + name: html-documentation + path: html/ -- cgit