Skip to content

Conversation

@jorisdral
Copy link
Contributor

No description provided.

@jorisdral jorisdral added the documentation Improvements or additions to documentation label Feb 8, 2023
@jorisdral jorisdral self-assigned this Feb 8, 2023
Copy link
Contributor

@jasagredo jasagredo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the explanation is reasonable and clarifies non-trivial stuff. I think this is OK.

@jorisdral jorisdral force-pushed the jdral/fingertree-rm-readme branch from cb97e3e to 96a4ad3 Compare February 9, 2023 12:33
@jorisdral jorisdral merged commit 8ea099d into main Feb 14, 2023
@jorisdral jorisdral deleted the jdral/fingertree-rm-readme branch February 14, 2023 15:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation Improvements or additions to documentation

Projects

No open projects
Status: ✅ Done

Development

Successfully merging this pull request may close these issues.

3 participants