diff options
| author | Leah Rowe <leah@libreboot.org> | 2023-05-14 11:21:56 +0100 |
|---|---|---|
| committer | Leah Rowe <leah@libreboot.org> | 2023-05-14 11:21:56 +0100 |
| commit | db3c1d9ccf64127e64f0bbce843c624c993a8eed (patch) | |
| tree | 856ac364aecbf707f2982a3595cc85ce4e55e8e3 /resources/grub | |
| parent | d90dfb0a08bcc82200227afd7ab3c0b2ab72a91e (diff) | |
download/grub: delete grub if gnulib cloning fails
for our purposes, grub and gnulib are one in the same
if one fails, both have failed
exit with non-zero status if gnulib fails
the script sets -e so it will fail if grub fails to
download, which is tried before gnulib, and if that
happens, the grub directory is not created
Diffstat (limited to 'resources/grub')
0 files changed, 0 insertions, 0 deletions