mirror/godot
2
0
Fork 0
mirror of https://github.com/godotengine/godot.git synced 2025-02-17 22:43:01 +08:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #28107 from Amssat221/issue28105

Browse Source 
Set range (10-50) to help source font size
This commit is contained in:
Rémi Verschelde 2019-05-28 11:53:52 +02:00 committed by GitHub
commit 58f66fa848
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
editor/editor_fonts.cpp
View File

@ -228,7 +228,7 @@ void editor_register_fonts(Ref<Theme> p_theme) {
p_theme->set_font("doc", "EditorFonts", df_doc);
p_theme->set_font("doc_title", "EditorFonts", df_doc_title);
MAKE_SOURCE_FONT(df_doc_code, int(EDITOR_DEF("text_editor/help/help_source_font_size", 14)) * EDSCALE);
MAKE_SOURCE_FONT(df_doc_code, int(EDITOR_GET("text_editor/help/help_source_font_size")) * EDSCALE);
p_theme->set_font("doc_source", "EditorFonts", df_doc_code);
// Ruler font

2
editor/editor_settings.cpp
View File

@ -487,6 +487,8 @@ void EditorSettings::_load_defaults(Ref<ConfigFile> p_extra_config) {
// Help
_initial_set("text_editor/help/show_help_index", true);
_initial_set("text_editor/help_source_font_size", 14);
hints["text_editor/help/help_source_font_size"] = PropertyInfo(Variant::REAL, "text_editor/help/help_source_font_size", PROPERTY_HINT_RANGE, "10, 50, 1");
/* Editors */