The option line may start with a space, which gives an empty option.

Make sure those are purged...
This commit is contained in:
Richard Levitte 2000-12-31 01:54:18 +00:00
parent 97f56446a3
commit 7f2113a2d5

View file

@ -81,7 +81,7 @@ EOF
}
$platform=$_;
}
foreach (split / /, $OPTIONS)
foreach (grep(!/^$/, split(/ /, $OPTIONS)))
{
print STDERR "unknown option - $_\n" if !&read_options;
}