update (CicleCI) CI script to work with ghc-ci
authorAlp Mestanogullari <alp@well-typed.com>
Wed, 28 Nov 2018 15:31:31 +0000 (16:31 +0100)
committerAlp Mestanogullari <alp@well-typed.com>
Sun, 2 Dec 2018 11:38:15 +0000 (12:38 +0100)
commit93a3f9070d5d69ad6a28fe94ccccd20c54609698
tree82473f4c040c36c30842948633505d4dbaa20900
parent93e86d6103757b43017535c92bc6970e9e2315a5
update (CicleCI) CI script to work with ghc-ci

ghc-ci is a tiny webservice that acts as an intermediate between our
CircleCI jobs on Gitlab and the actual builds running on CircleCI, so that
the build script doesn't need to rely on any secret, which makes the whole
setup fork-friendly.

The concrete effect of this patch is to allow any fork of GHC on Gitlab to
run CircleCI jobs.
.gitlab-ci.yml
.gitlab/circle-ci-job.sh