diff options
Diffstat (limited to 'tools/options.py')
| -rw-r--r-- | tools/options.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/options.py b/tools/options.py index edc39d5e75..0840deed81 100644 --- a/tools/options.py +++ b/tools/options.py @@ -38,7 +38,7 @@ def AddOptions(): action = 'store_true', default = False, help = 'make distribution and strip useless files') - AddOption('--dist-ide', + AddOption('--dist-ide', '--dist-rtstudio', dest = 'make-dist-ide', action = 'store_true', default = False, |