Christian Prochaska 63ebebcfa4 nitpicker: update the 'pointed session' more often ... Currently, the 'pointed session' gets updated only when an input event occurs, but an update is also needed in other situations, for example when the view under the current mouse position was moved. With this commit, the 'pointed session' gets updated whenever the timer-triggered 'handle_input()' function is called. Fixes #1473		2015-04-13 14:18:15 +02:00
..
app	os: make reusable cli_monitor headers public	2014-10-13 15:21:54 +02:00
drivers	SD-card driver for the Raspberry Pi	2015-04-09 16:04:47 +02:00
init	Init: support for aliases for child names	2015-01-20 11:25:59 +01:00
lib	Improve 'Timed_semaphore' accuracy	2015-02-27 11:48:07 +01:00
server	nitpicker: update the 'pointed session' more often	2015-04-13 14:18:15 +02:00
test	base: extend emergency dataspace size	2015-04-09 16:04:46 +02:00