From 53190e6160414c5ee1caee6edcebc95c686f140b Mon Sep 17 00:00:00 2001
From: Gilles Peskine <Gilles.Peskine@arm.com>
Date: Wed, 9 Jan 2019 23:17:35 +0100
Subject: [PATCH] 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.
---
 tests/scripts/all.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/scripts/all.sh b/tests/scripts/all.sh
index 642128af2..b95429b29 100755
--- a/tests/scripts/all.sh
+++ b/tests/scripts/all.sh
@@ -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