diff options
author | Matthew Pickering <matthewtpickering@gmail.com> | 2018-08-21 08:34:50 +0100 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2018-08-21 19:12:39 -0400 |
commit | 3902a807acf4bccf5cd01d2115bed10d57316661 (patch) | |
tree | 12cdc2a48d3f55ff6b6bf521f98e3dc04977f87b /haddock-api/resources/html/Ocean.theme/plus.gif | |
parent | 40eb5aabed0ae52982a690be311177b2dea2a0bb (diff) |
Load plugins when starting a GHC session (#905)
Fixes #900
(cherry picked from commit e6aa8fb47b9477cc5ef5e46097524fe83e080f6d)
Diffstat (limited to 'haddock-api/resources/html/Ocean.theme/plus.gif')
0 files changed, 0 insertions, 0 deletions