Add option learn-ocaml build serve --serve-during-build and fix related minor issues
#298
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: check-update-index | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - '**' | |
| jobs: | |
| check-index: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v4 | |
| - name: Execute the script | |
| run: ./scripts/update-index.sh | |
| - name: Check the diff | |
| run: echo diff_output="$(git diff --name-only "$PWD/docs/index.md")" >> "$GITHUB_ENV" | |
| - name: Warning | |
| # if diff_output not null and master branch | |
| if: env.diff_output != '' && github.ref_name == 'master' | |
| run: "echo ::warning:: 'docs/index.md' outdated, please run 'scripts/update-index.sh'." | |
| - name: Error | |
| # if diff_output not null and not master branch | |
| if: env.diff_output != '' && github.ref_name != 'master' | |
| run: "echo ::error:: 'docs/index.md' outdated, please run 'scripts/update-index.sh' and commit.; exit 1" |