diff --git a/templates/seL4VMParameters.template.c b/templates/seL4VMParameters.template.c index 797d4bae..0cb20e54 100644 --- a/templates/seL4VMParameters.template.c +++ b/templates/seL4VMParameters.template.c @@ -8,10 +8,11 @@ #include #include -/*- set vm_address_config = configuration[me.name].get('vm_address_config') -*/ -/*- set vm_image_config = configuration[me.name].get('vm_image_config') -*/ -/*- set linux_address_config = configuration[me.name].get('linux_address_config') -*/ -/*- set linux_image_config = configuration[me.name].get('linux_image_config') -*/ +/*- set config = configuration[me.name] -*/ +/*- set vm_address_config = config.get('vm_address_config') -*/ +/*- set vm_image_config = config.get('vm_image_config') -*/ +/*- set linux_address_config = config.get('linux_address_config') -*/ +/*- set linux_image_config = config.get('linux_image_config') -*/ /*# For legacy compatibility, a fall back to the standard Linux entry exists. #*/ /*- set is_64_bit = (8 == macros.get_word_size(options.architecture)) -*/