diff options
Diffstat (limited to '.gitlab')
| -rwxr-xr-x | .gitlab/ci.sh | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh index 6dd12768b1..c447696ae6 100755 --- a/.gitlab/ci.sh +++ b/.gitlab/ci.sh @@ -214,8 +214,6 @@ function set_toolchain_paths() { cat toolchain.sh fi source toolchain.sh - info "--info for GHC for $NIX_SYSTEM" - $GHC --info ;; env) # These are generally set by the Docker image but @@ -274,6 +272,11 @@ function setup() { show_tool CABAL show_tool HAPPY show_tool ALEX + + info "=====================================================" + info "ghc --info" + info "=====================================================" + $GHC --info } function fetch_ghc() { |