genode/tool/run/log.inc
2015-01-26 12:28:40 +01:00

8 lines
124 B
PHP

##
# Get the spawn_id of the output process
#
proc output_spawn_id { } {
global output_spawn_id
return $output_spawn_id
}