[env] remove --dist-strip command

2025-10-20 05:25:04 +08:00 · 2023-09-14 18:40:45 -04:00
parent e7c3ca61fd
commit c19c907b62
3 changed files with 1 additions and 136 deletions
--- 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',