Delete $OUT_OF_SOURCE_DIR under --force

The deletion of "$OUT_OF_SOURCE_DIR" had mistakenly been lumped
together with Yotta and then removed when Yotta support was removed.
Bring it back.
This commit is contained in:
Gilles Peskine 2019-01-09 23:17:35 +01:00
parent add1d23b26
commit d692e11309

View file

@ -370,6 +370,7 @@ pre_parse_command_line () {
pre_check_git () {
if [ $FORCE -eq 1 ]; then
rm -rf "$OUT_OF_SOURCE_DIR"
git checkout-index -f -q $CONFIG_H
cleanup
else