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

(Support changing abbreviation letter) Support writing math symbols using ; in addition to \ #225

Open
JadAbouHawili opened this issue May 5, 2024 · 1 comment
Open

(Support changing abbreviation letter) Support writing math symbols using ; in addition to \ #225

JadAbouHawili opened this issue May 5, 2024 · 1 comment
Labels
client Functionality of the client side code enhancement New feature or request priority-low nice to have

Comments

@JadAbouHawili
Copy link
Contributor

The ; button is easier to reach, and it's allowed in vscode so why not.
@joneugster joneugster added enhancement New feature or request client Functionality of the client side code priority-low nice to have labels May 5, 2024
@joneugster
Copy link
Collaborator

I believe it's only a thing in vscode if you set it in the settings. But I agree, lean4web has the option to choose the abbreviation character. Would be nice to integrate the settings from there.

@JadAbouHawili JadAbouHawili changed the title Support writing math symbols using ; in addition to \ (Support changing abbreviation letter) Support writing math symbols using ; in addition to \ Jul 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
client Functionality of the client side code enhancement New feature or request priority-low nice to have
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@joneugster @JadAbouHawili