mirror of
https://github.com/genodelabs/genode.git
synced 2024-12-30 10:38:55 +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 |
||
---|---|---|
.. | ||
api | ||
pkg | ||
raw | ||
src |