diff options
| -rw-r--r-- | scripts/lib/devtool/standard.py | 11 |
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 |