File tree Expand file tree Collapse file tree 1 file changed +2
-3
lines changed Expand file tree Collapse file tree 1 file changed +2
-3
lines changed Original file line number Diff line number Diff line change 1-
21name : Build & update docs
32
43on :
4645
4746 - name : Build docs
4847 run : |
49- make -C docs/ SPHINXOPTS="-W" BUILDDIR="$HOME/docs" OUTDIR="${CURBRANCH:-html}" html
48+ make -C docs/ SPHINXOPTS="-W" BUILDDIR="$HOME/docs" OUTDIR="${CURBRANCH:-html}" html
5049
5150 - name : Push created tag to gh-pages
5251 if : startsWith(github.ref, 'refs/tags/')
7069 - name : Push "main" docs to gh-pages after a PR is merged
7170 if : github.ref == 'refs/heads/master' || github.ref == 'refs/heads/main'
7271 run : |
73- if [[ "${CURBRANCH}" != "master" -a "${CURBRANCH}" != "main" ]]; then
72+ if [[ "${CURBRANCH}" != "master" && "${CURBRANCH}" != "main" ]]; then
7473 echo "$CURBRANCH is not the default development branch"
7574 exit 1
7675 fi
You can’t perform that action at this time.
0 commit comments