Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Document docstrings in RM #3771

Closed
davidcok opened this issue Mar 21, 2023 · 1 comment · Fixed by #3773
Closed

Document docstrings in RM #3771

davidcok opened this issue Mar 21, 2023 · 1 comment · Fixed by #3773
Labels
part: documentation Dafny's reference manual, tutorial, and other materials

Comments

@davidcok
Copy link
Collaborator

What change in documentation do you suggest?

docsstrings need to be described in the RM
@davidcok davidcok added the part: documentation Dafny's reference manual, tutorial, and other materials label Mar 21, 2023
@davidcok davidcok mentioned this issue Apr 22, 2023
Merged
@davidcok
Copy link
Collaborator Author

Fixed by PR #3773

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
part: documentation Dafny's reference manual, tutorial, and other materials
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Documentation on docstrings davidcok/dafny
1 participant
@davidcok