Anthony Gitter

> will there be an easy way to delete versions for closed PRs? I could imagine having a scheduled workflow that does a nightly cleanup of the pull request builds...

In #221 @slochower discusses the pros and cons of using Hypothesis for rapid, publicly visible, concurrent feedback on a draft. See especially his notes in https://github.com/manubot/rootstock/issues/221#issuecomment-494954571 about using groups or...

> Handling PRs from people not familiar with GitHub requires that I ask permission to commit to their PRs before merging (or merge their PRs and do cleanup afterwards). Could...

@dhimmel I didn't have any specific idea for how to make every line reviewable, yours is the first. I was thinking of adding comments with special characters between paragraphs (or...

I'm not aware of any such utilities, but I haven't looked. I'm tagging @rando2 because she has been interested in two-way conversion between markdown and docx for collaborative manuscripts that...

Interesting. The "Comment on Pull Request" step failed with a 403 forbidden error in this pull request. The same workflow worked when I made a pull request into a repository...

The GitHub developer guide refers to a personal access token for authentication: https://developer.github.com/v3/guides/working-with-comments/#pull-request-comments If I'm reading the [`GITHUB_TOKEN` permissions](https://help.github.com/en/actions/configuring-and-managing-workflows/authenticating-with-the-github_token#permissions-for-the-github_token) correctly, it shows forked repos only have read permission.

> do you have any insight? Sorry, I have no ideas about the best font.

> ₿ != ฿ Same behavior for me in both browsers I tested

The tables in #215 would be great for the front end. I've been thinking about this more, and the real functionality needed to support what I had in mind might...