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 d1174cf015
commit 53190e6160

View File

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