diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2019-05-20 22:39:19 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-05-20 22:39:19 +0200 |
| commit | 63e7d2db08ff7a2fafdf99c635ab985b9b0278f8 (patch) | |
| tree | eec89f7059cec7ab6b91bb7ebc4fc188c6bfe5fe /editor/plugins/text_editor.h | |
| parent | defd9602764c13d1b7753cf879bdbcdf56335b33 (diff) | |
| parent | 0bfcf8bc2fb9b863db81c1c8055a250206080c70 (diff) | |
Merge pull request #28218 from KoBeWi/b00km4rk5
Add bookmarks for easier code navigation
Diffstat (limited to 'editor/plugins/text_editor.h')
| -rw-r--r-- | editor/plugins/text_editor.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/editor/plugins/text_editor.h b/editor/plugins/text_editor.h index 767001e2f6..2da7474793 100644 --- a/editor/plugins/text_editor.h +++ b/editor/plugins/text_editor.h @@ -87,6 +87,10 @@ private: SEARCH_FIND_PREV, SEARCH_REPLACE, SEARCH_GOTO_LINE, + BOOKMARK_TOGGLE, + BOOKMARK_GOTO_NEXT, + BOOKMARK_GOTO_PREV, + BOOKMARK_REMOVE_ALL, }; protected: |