1 files changed, 5 insertions, 0 deletions

diff --git a/repo b/repo
index 0aabc0d89..860a15d5e 100755
--- a/repo
+++ b/repo
@@ -129,6 +129,11 @@ group.add_option('-g', '--groups',
                  dest='groups', default='default',
                  help='restrict manifest projects to ones with a specified group',
                  metavar='GROUP')
+group.add_option('-p', '--platform',
+                 dest='platform', default="auto",
+                 help='restrict manifest projects to ones with a specified'
+                      'platform group [auto|all|none|linux|darwin|...]',
+                 metavar='PLATFORM')
 
 
 # Tool