Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
We again build documentation in case of proper source errors (#253)
and only refuse building it in case of "GHC server died (dummy error)". We are in no position to decide if partial documentation should be built or not. Let the user of our API decide --- he has access to all relevant information, in particular, to errors.
- Loading branch information