diff options
| author | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2015-02-24 17:35:49 -0500 |
|---|---|---|
| committer | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2015-02-24 23:33:45 -0500 |
| commit | 1d64e14c30e993c2d3dc948fe53118d8700c3ade (patch) | |
| tree | d5fd176391ee2d27b7a74b4520a1adee9832b1b9 /src/random-seed | |
| parent | 7cb0f263adacbd12f5be4f7f23d7f596485adb37 (diff) | |
build-sys: fail if gnuefi files are not found
The build would fail later anyway, so it is better to bail
out early.
Also check for the second bios file only if the first one was not
found. I'm not sure which one is preferred. If the other one, the
order should be flipped.
Diffstat (limited to 'src/random-seed')
0 files changed, 0 insertions, 0 deletions