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.

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

Add Formatter Option to Replace Unicode Symbols with ASCII Variants #2082

Open
jonaprieto opened this issue May 11, 2023 · 0 comments
Open
Assignees
Milestone

Comments

@jonaprieto
Copy link
Collaborator

jonaprieto commented May 11, 2023

This feature can be particularly useful when using fonts that do not support certain Unicode symbols. The proposed command for this operation is

juvix format --no-unicode File.juvix

Feel free to suggest another name for this flag. This feature should be optional, not the default behaviour, to maintain the versatility of the tool and accommodate various user preferences.

Related:

@jonaprieto jonaprieto added this to the 0.4.1 milestone May 11, 2023
@paulcadman paulcadman modified the milestones: 0.4.1, 0.4.2 Jun 23, 2023
@jonaprieto jonaprieto modified the milestones: 0.4.2, 0.4.3 Jul 24, 2023
@jonaprieto jonaprieto modified the milestones: 0.4.3, 0.4.4 Aug 24, 2023
@jonaprieto jonaprieto modified the milestones: 0.4.4, 0.5 Sep 7, 2023
@lukaszcz lukaszcz modified the milestones: 0.5.0, 0.5.2 Sep 15, 2023
@jonaprieto jonaprieto modified the milestones: 0.5.2, 0.5.3 Oct 2, 2023
@jonaprieto jonaprieto modified the milestones: 0.5.3, 0.5.4 Oct 31, 2023
@jonaprieto jonaprieto self-assigned this Nov 6, 2023
@jonaprieto jonaprieto modified the milestones: 0.5.4, 0.5.5 Nov 17, 2023
@jonaprieto jonaprieto modified the milestones: 0.5.5, 0.5.6 Dec 1, 2023
@jonaprieto jonaprieto modified the milestones: 0.5.6, 0.6.1 Mar 9, 2024
@paulcadman paulcadman removed this from the 0.6.1 milestone Mar 25, 2024
@paulcadman paulcadman added this to the 0.6.2 milestone Mar 25, 2024
@paulcadman paulcadman modified the milestones: 0.6.2, 0.6.3 Jun 12, 2024
@paulcadman paulcadman modified the milestones: 0.6.3, 0.6.4 Jul 2, 2024
@paulcadman paulcadman modified the milestones: 0.6.4, 0.6.5 Jul 19, 2024
@paulcadman paulcadman modified the milestones: 0.6.5, 0.6.6 Aug 15, 2024
@lukaszcz lukaszcz modified the milestones: 0.6.6, 0.6.7 Sep 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants