Skip to content

Rightarrow fixes and other small doc fixes#1400

Merged
rocky merged 1 commit intomasterfrom
implies-doc-symbol
Jun 3, 2021
Merged

Rightarrow fixes and other small doc fixes#1400
rocky merged 1 commit intomasterfrom
implies-doc-symbol

Conversation

@rocky
Copy link
Copy Markdown
Member

@rocky rocky commented Jun 1, 2021

Makefile: add "doc" target.
Correct Standard Unicode code for rightarrow and make that pass through.

@rocky rocky requested a review from mmatera June 1, 2021 23:46
Makefile: add "doc" target.
Correct Standard Unicode code for rightarrow and make that pass through.
@rocky rocky force-pushed the implies-doc-symbol branch from fe1cae9 to 0a48c80 Compare June 1, 2021 23:47
@rocky rocky merged commit ee072c8 into master Jun 3, 2021
@rocky rocky deleted the implies-doc-symbol branch June 6, 2021 20:57
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.

1 participant