Docs for some of DocH's less intuitive constructors

[sjakobi]

No description provided.

[alexbiehl]

Thanks Simon! I don't mind if you push directly to master for small changes like these.

[sjakobi]

Thanks Simon! I don't mind if you push directly to master for small changes like these.

Will do. To master or to ghc-8.4 though?

(If master currently has no use, I'd propose deleting it to reduce confusion.)

[alexbiehl]

Ah right. Let's delete master.

[sjakobi]

Can you remove the branch protection on master?

[sjakobi]

Gosh, sorry for the mess with the pull requests. I can clean this up by retargeting to the ghc-8.4 branch.

[sjakobi]

The affected PRs are #670, #729, #721, #728, #708, #562, #700 and #692 (replaced by #822).

[ntc2]

@sjakobi , @alexbiehl : looks like all of the PRs mentioned in @sjakobi 's last comment just got closed, but it's unclear why. Could someone explain what's going on?

[sjakobi]

@ntc2: The master branch was deleted as it didn't have a clear function in this repo. What @alexbiehl and I hadn't considered, was that GitHub would automatically close all PRs targeting the master branch.

To reopen an affected PR, you can try changing the merge target to the ghc-8.4 branch by clicking the Edit button to the right of the PR's title. Some PRs may have to be rebased.

[ntc2]

@sjakobi Ah! I just commented on all of those issues pointing back to your explanation, in case others are confused.

[sjakobi]

Thanks for helping out with this mishap, @ntc2! As #700 seems to show, simply retargeting the PR doesn't appear to work. :/

Hopefully rebasing will work for the affected PRs. As a last resort, submitters can open a new one. :/