diff options
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', |