Merge pull request #42211 from dje4321/dje4321

Grub: default is signed int. Fixes #42152
This commit is contained in:
Jörg Thalheim 2018-06-19 10:55:13 +01:00 committed by GitHub
commit 81eaa7ab1b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 4 additions and 3 deletions

View File

@ -385,8 +385,9 @@ in
}; };
default = mkOption { default = mkOption {
default = 0; default = "0";
type = types.int; type = types.either types.int types.str;
apply = toString;
description = '' description = ''
Index of the default menu item to be booted. Index of the default menu item to be booted.
''; '';

View File

@ -54,7 +54,7 @@ my $splashImage = get("splashImage");
my $configurationLimit = int(get("configurationLimit")); my $configurationLimit = int(get("configurationLimit"));
my $copyKernels = get("copyKernels") eq "true"; my $copyKernels = get("copyKernels") eq "true";
my $timeout = int(get("timeout")); my $timeout = int(get("timeout"));
my $defaultEntry = int(get("default")); my $defaultEntry = get("default");
my $fsIdentifier = get("fsIdentifier"); my $fsIdentifier = get("fsIdentifier");
my $grubEfi = get("grubEfi"); my $grubEfi = get("grubEfi");
my $grubTargetEfi = get("grubTargetEfi"); my $grubTargetEfi = get("grubTargetEfi");