1 files changed, 11 insertions, 0 deletions

diff --git a/scripts/lib/devtool/standard.py b/scripts/lib/devtool/standard.py
index ed9e793d4a..a9c4cf8d8d 100644
--- a/scripts/lib/devtool/standard.py
+++ b/scripts/lib/devtool/standard.py
@@ -1229,6 +1229,17 @@ def reset(args, config, basepath, workspace):
         # We don't automatically create this dir next to appends, but the user can
         preservedir(os.path.join(config.workspace_path, 'appends', pn))
 
+        srctree = workspace[pn]['srctree']
+        if os.path.isdir(srctree):
+            if os.listdir(srctree):
+                # We don't want to risk wiping out any work in progress
+                logger.info('Leaving source tree %s as-is; if you no '
+                            'longer need it then please delete it manually'
+                            % srctree)
+            else:
+                # This is unlikely, but if it's empty we can just remove it
+                os.rmdir(srctree)
+
     return 0