diff options
Diffstat (limited to 'extras/mini-os/domain_config')
| -rw-r--r-- | extras/mini-os/domain_config | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/extras/mini-os/domain_config b/extras/mini-os/domain_config index d6635c88f9..57f909ac5d 100644 --- a/extras/mini-os/domain_config +++ b/extras/mini-os/domain_config @@ -15,3 +15,5 @@ memory = 32 # A name for your domain. All domains must have different names. name = "Mini-OS" + +on_crash = 'destroy' |