diff options
| author | Meco Man <[email protected]> | 2023-09-14 18:40:45 -0400 |
|---|---|---|
| committer | Meco Man <[email protected]> | 2023-09-15 08:52:48 -0400 |
| commit | c19c907b62e241b0649673e8cfd02bb46f48d18c (patch) | |
| tree | ea4abd27354ae0759e3ff756e0fbb856312a5003 /tools/options.py | |
| parent | e7c3ca61fd2a13fe8d1623e7cdd215f17eedf13c (diff) | |
[env] remove --dist-strip command
Diffstat (limited to 'tools/options.py')
| -rw-r--r-- | tools/options.py | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tools/options.py b/tools/options.py index 439f13c6b5..9d8c0ff4df 100644 --- a/tools/options.py +++ b/tools/options.py @@ -33,11 +33,6 @@ def AddOptions(): action = 'store_true', default = False, help = 'make distribution') - AddOption('--dist-strip', - dest = 'make-dist-strip', - action = 'store_true', - default = False, - help = 'make distribution and strip useless files') AddOption('--dist-ide', '--dist-rtstudio', dest = 'make-dist-ide', action = 'store_true', |