Skip to content

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

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

How to change the editor's font? #45

Closed
ghost opened this issue Nov 27, 2022 · 1 comment
Closed

How to change the editor's font? #45

ghost opened this issue Nov 27, 2022 · 1 comment

Comments

@ghost
Copy link

ghost commented Nov 27, 2022

I wanted to change it to something else but I can't find where the setting is.

@ghost ghost closed this as completed Nov 27, 2022
@fredvs
Copy link
Owner

fredvs commented Nov 27, 2022

The font of editor is defined by the project options:

project-ideu

If you prefer to have your own config for all projects, independent of the options of the project, go to menu / Settings / Extra settings and, in right side of window, select in Source Editor: "X Use those options instead of project options".
And set all the values that follow like you want.

set-editor-ideu

Repository owner locked and limited conversation to collaborators Nov 28, 2022
@fredvs fredvs converted this issue into discussion #59 Nov 28, 2022

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant