mirror of
https://github.com/genodelabs/genode.git
synced 2024-12-27 09:12:32 +00:00
0f54ad8e26
This patch moves the text-editing facility of app/text_area to a text-area widget as part of the dialog library. This has two benefits. First, it simplifies app/text_area by using the dialog API. Second, the editor can now easily be reused by other dialog-API-based applications. Fixes #5058 |
||
|---|---|---|
| .. | ||
| import | ||
| mk | ||
| symbols | ||