diff options
author | Timothee Cour <timothee.cour2@gmail.com> | 2021-04-30 22:24:41 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-01 07:24:41 +0200 |
commit | 1f1d85bb9c614d93ce38becdcc421dda00264a75 (patch) | |
tree | 1e012ea3f6bb45383451fc79bfe369702a33bf5d /.github | |
parent | abb8a73134597297b2c14567f7f8d72f6b723d24 (diff) | |
download | Nim-1f1d85bb9c614d93ce38becdcc421dda00264a75.tar.gz |
reuse config/build_config.txt for all bootstrap scripts (posix + windows + ci); use build_all.bat in 1 CI, fix bug in build_all.bat (#17899)
* reuse config/build_config.txt for all bootstrap scripts (posix + windows + ci) * ci_docs: use build_all.bat in CI (just in that pipeline) to ensure it keeps working * fixup * fix pre-existing bug in build_all.bat * fixup * cp => copy /y * auto-generate build_all.bat, build_all.sh * fixup
Diffstat (limited to '.github')
-rw-r--r-- | .github/workflows/ci_docs.yml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/.github/workflows/ci_docs.yml b/.github/workflows/ci_docs.yml index 1459d6a31..dfcff66e0 100644 --- a/.github/workflows/ci_docs.yml +++ b/.github/workflows/ci_docs.yml @@ -70,13 +70,21 @@ jobs: shell: bash run: echo "${{ github.workspace }}/bin" >> "${GITHUB_PATH}" - - name: 'Build csourcesAny' + - name: 'Build csourcesAny (posix)' + # this would work on windows and other CI use this on windows, + # but we ensure here that `ci/build_autogen.bat` keeps working on windows. + if: runner.os != 'Windows' shell: bash run: . ci/funs.sh && nimBuildCsourcesIfNeeded CC=gcc # was previously using caching via `actions/cache@v1` but this wasn't # used in other CI pipelines and it's unclear the added complexity # was worth the saving; can be revisited if needed. + - name: 'Build csourcesAny (windows)' + if: runner.os == 'Windows' + shell: cmd + run: ci/build_autogen.bat + - name: 'Build koch' shell: bash run: nim c koch |