Skip to content

Replace twiddle with tilde#443

Merged
rok-cesnovar merged 1 commit intomasterfrom
twiddle_to_tilde
Nov 22, 2021
Merged

Replace twiddle with tilde#443
rok-cesnovar merged 1 commit intomasterfrom
twiddle_to_tilde

Conversation

@rok-cesnovar
Copy link
Copy Markdown
Member

Summary

In pedantic mode docs, we use the word twiddle instead of tilde. I know they are considered synonyms, but given that we used tilde everywhere else (parser, docs, etc), it should be tilde here as well.

Copyright and Licensing

Please list the copyright holder for the work you are submitting (this will be you or your assignee, such as a university or company):
Rok Češnovar

By submitting this pull request, the copyright holder is agreeing to license the submitted work under the following licenses:

@rok-cesnovar rok-cesnovar merged commit 91c1c0e into master Nov 22, 2021
@rok-cesnovar rok-cesnovar deleted the twiddle_to_tilde branch November 22, 2021 20:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants