alex/genode-world
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Rename "Nitpicker" service name to "Gui"

Browse Source 
Issue genodelabs/genode#3778
This commit is contained in:
Norman Feske
2020-06-11 16:07:18 +02:00
parent 7c92181da4
commit 46a588a0b1
12 changed files with 25 additions and 25 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
run/flif.run
View File

@@ -52,7 +52,7 @@ install_config {
<start name="nitpicker">
<resource name="RAM" quantum="4M"/>
<provides><service name="Nitpicker"/></provides>
<provides><service name="Gui"/></provides>
<config>
<domain name="pointer" layer="1" content="client" label="no" origin="pointer" />
<domain name="default" layer="2" content="client" label="no" hover="always" focus="click" />
@@ -65,7 +65,7 @@ install_config {
<start name="pointer">
<resource name="RAM" quantum="1M"/>
<route>
<service name="Nitpicker"> <child name="nitpicker"/> </service>
<service name="Gui"> <child name="nitpicker"/> </service>
<any-service> <parent/> <any-child/> </any-service>
</route>
</start>