diff options
| author | Jason Gross | 2017-06-26 11:09:06 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-07-21 03:36:47 -0400 |
| commit | 987655c3bc8a8ebd60856356f465b3c34eb4e252 (patch) | |
| tree | f41062a6a59d1fba4b655c564e54563cb7f3d1d7 /dev/ci/ci-hott.sh | |
| parent | a0c84abf1f3078c1ba42df1b588acbac4bc2e4df (diff) | |
Separate make from python script for HoTT
HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does
Diffstat (limited to 'dev/ci/ci-hott.sh')
| -rwxr-xr-x | dev/ci/ci-hott.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index aa2edff7aa..c905558532 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -6,5 +6,6 @@ source ${ci_dir}/ci-common.sh HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} +( cd ${HoTT_CI_DIR} && git submodule update --init --recursive ) -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && git submodule update --init --recursive && ./etc/coq-scripts/timing/make-pretty-timed-or-error.sh ) +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && (make TIMED=1 | tee time-of-build.log; exit ${PIPESTATUS[0]}) && python ./etc/coq-scripts/timing/make-one-time-file.py time-of-build.log time-of-build-pretty.log && cat time-of-build-pretty.log ) |