diff options
Diffstat (limited to 'extras/mini-os/domain_config')
| -rw-r--r-- | extras/mini-os/domain_config | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/extras/mini-os/domain_config b/extras/mini-os/domain_config index 57f909ac5d..f3ec1d1c51 100644 --- a/extras/mini-os/domain_config +++ b/extras/mini-os/domain_config @@ -8,7 +8,7 @@ #---------------------------------------------------------------------------- # Kernel image file. -kernel = "mini-os.elf" +kernel = "mini-os.gz" # Initial memory allocation (in megabytes) for the new domain. memory = 32 |