Skip to content

Tolerate Unicode DifferentialD#1575

Merged
rocky merged 1 commit intomasterfrom
DifferentialD-adjust
Sep 11, 2021
Merged

Tolerate Unicode DifferentialD#1575
rocky merged 1 commit intomasterfrom
DifferentialD-adjust

Conversation

@rocky
Copy link
Copy Markdown
Member

@rocky rocky commented Sep 4, 2021

We are in the process of preferring Unicode symbols over custom WL
symbols on input (when they are different) since our frontends
use standard Unicode when they support Unicode.

We are in the process of preferring Unicode symbols over custom WL
symbols on input (when they are different) since our frontends
use standard Unicode when they support Unicode.
@rocky rocky requested a review from mmatera September 4, 2021 23:01
@rocky rocky merged commit b984aa5 into master Sep 11, 2021
@rocky rocky deleted the DifferentialD-adjust branch September 11, 2021 14:29
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