Closed tirix closed 3 years ago
@tirix - makes sense to me. Merge at your convenience.
@digama0 can merge, then. I don't have the write access!
@tirix - check your mailbox & accept the invitation to become a contributor. It may be in your junk folder. You've been invited to become a contributor (and thus have direct rights) but you haven't accepted.
Thanks David! I found the invitation but unfortunately it had expired. Could you please send it again?
@tirix - you've been re-invited! My hope is that you'll post PRs, give people a little time to comment, then merge after thinking through the comments.
I imagine we'll eventually move this to the metamath project, but that's a separate conversation.
Thank you very much for the invitation! I've merged this commit.
My hope is that you'll post PRs, give people a little time to comment.
I most definitely will. I've already opened the PR #16 for the next batch of changes, you can already have a look.
I forgot to isolate this part in #14