diff options
| author | Herbert Valerio Riedel <hvr@gnu.org> | 2018-06-20 23:32:41 +0200 |
|---|---|---|
| committer | Herbert Valerio Riedel <hvr@gnu.org> | 2018-06-20 23:32:41 +0200 |
| commit | 9339517a2bd1c16c1d11e66d9c754f0ef702f99a (patch) | |
| tree | 95e5317ea2df5ab6dc866aa650d1859bf8c43b2c /html-test/ref/mini_TitledPicture.html | |
| parent | ef16b9f8f73e6a4d639919152925ab83d9b1024f (diff) | |
Drop GHC HEAD from CI and update GHC to 8.4.3
It's a waste of resource to even try to build this branch w/ ghc-head;
so let's not do that...
Diffstat (limited to 'html-test/ref/mini_TitledPicture.html')
0 files changed, 0 insertions, 0 deletions