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 createdfsdg20230625
parent
d90dfb0a08
commit
db3c1d9ccf
|
@ -2,7 +2,8 @@
|
||||||
|
|
||||||
# helper script: Downloads GRUB and patches it.
|
# helper script: Downloads GRUB and patches it.
|
||||||
#
|
#
|
||||||
# Copyright (C) 2014, 2015, 2016, 2020, 2021 Leah Rowe <info@minifree.org>
|
# Copyright (C) 2014,2015,2016,2020,2021,2023 Leah Rowe
|
||||||
|
# <info@minifree.org>
|
||||||
#
|
#
|
||||||
# This program is free software: you can redistribute it and/or modify
|
# This program is free software: you can redistribute it and/or modify
|
||||||
# it under the terms of the GNU General Public License as published by
|
# it under the terms of the GNU General Public License as published by
|
||||||
|
@ -22,4 +23,10 @@
|
||||||
set -u -e
|
set -u -e
|
||||||
|
|
||||||
./gitclone grub
|
./gitclone grub
|
||||||
./gitclone gnulib
|
./gitclone gnulib || rm -Rf grub/
|
||||||
|
if [ ! -d grub ]; then
|
||||||
|
printf "%s: Could not download grub and gnulib\n" ${0}
|
||||||
|
exit 1
|
||||||
|
else
|
||||||
|
exit 0
|
||||||
|
fi
|
||||||
|
|
Loading…
Reference in New Issue