diff --git a/repos/ports/run/virtualbox.run b/repos/ports/run/virtualbox.run index 82efb64f7..6ee2ef9cd 100644 --- a/repos/ports/run/virtualbox.run +++ b/repos/ports/run/virtualbox.run @@ -7,6 +7,7 @@ set build_components { core init virtualbox drivers/framebuffer drivers/timer + server/report_rom } source ${genode_dir}/repos/base/run/platform_drv.inc @@ -58,9 +59,15 @@ append_if [expr $use_ps2] config { append_if [expr $use_usb] config { - + + + + + + + } @@ -104,6 +111,19 @@ append_if [expr $use_serial] config { } append config { + + + + + + + + + + + + + @@ -120,6 +140,13 @@ append config { + + + + + + + } @@ -128,7 +155,7 @@ install_config $config exec cp ${genode_dir}/repos/ports/run/test.vbox bin/. -set boot_modules { core init timer virtualbox test.iso test.vbox } +set boot_modules { core init timer virtualbox test.iso test.vbox report_rom } # platform-specific modules lappend_if [expr $use_usb] boot_modules usb_drv