diff options
| author | Tuncer Ayaz <tuncer.ayaz@gmail.com> | 2019-11-19 15:10:47 +0000 |
|---|---|---|
| committer | Tuncer Ayaz <tuncer.ayaz@gmail.com> | 2019-11-21 20:08:03 +0000 |
| commit | d641585679344796c39a7562fa844bb836da4f21 (patch) | |
| tree | 479ccacb41b3fd7de1d3345f19902fd70a10d173 /python/servo/command_base.py | |
| parent | ba3169e65d673f019ad1d59f24598d9e2eaae455 (diff) | |
| download | servo-d641585679344796c39a7562fa844bb836da4f21.tar.gz servo-d641585679344796c39a7562fa844bb836da4f21.zip | |
Implement `./mach check --media-stack`
While at it, extract --media-stack flag into command_base.py.
Diffstat (limited to 'python/servo/command_base.py')
| -rw-r--r-- | python/servo/command_base.py | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/python/servo/command_base.py b/python/servo/command_base.py index 42385ff4e38..f9a01bbb4af 100644 --- a/python/servo/command_base.py +++ b/python/servo/command_base.py @@ -793,6 +793,12 @@ install them, let us know by filing a bug!") help='Cross compile for given target platform', ), CommandArgument( + '--media-stack', + default=None, + choices=["gstreamer", "dummy"], + help='Which media stack to use', + ), + CommandArgument( '--android', default=None, action='store_true', |