diff options
| author | Simon Sapin <simon.sapin@exyr.org> | 2020-07-06 17:34:17 +0200 |
|---|---|---|
| committer | Simon Sapin <simon.sapin@exyr.org> | 2020-07-06 17:34:17 +0200 |
| commit | 1a8c5fed6f53b2a4b5ed120193acd10a4ffcb2c6 (patch) | |
| tree | 792d2537168e798e6c28f9c6279ac9ddc1f3a3f8 /python/servo/command_base.py | |
| parent | 637c6c0aec201055a82a47e976b5d872356aaee7 (diff) | |
| download | servo-1a8c5fed6f53b2a4b5ed120193acd10a4ffcb2c6.tar.gz servo-1a8c5fed6f53b2a4b5ed120193acd10a4ffcb2c6.zip | |
Add `.servobuild` configuration for the choice of media stack
Diffstat (limited to 'python/servo/command_base.py')
| -rw-r--r-- | python/servo/command_base.py | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/python/servo/command_base.py b/python/servo/command_base.py index 47fe9abd91a..f25721a5652 100644 --- a/python/servo/command_base.py +++ b/python/servo/command_base.py @@ -304,6 +304,7 @@ class CommandBase(object): self.config["build"].setdefault("debug-assertions", False) self.config["build"].setdefault("debug-mozjs", False) self.config["build"].setdefault("layout-2020", False) + self.config["build"].setdefault("media-stack", "auto") self.config["build"].setdefault("ccache", "") self.config["build"].setdefault("rustflags", "") self.config["build"].setdefault("incremental", None) @@ -856,11 +857,13 @@ install them, let us know by filing a bug!") # A guess about which platforms should use the gstreamer media stack def pick_media_stack(self, media_stack, target): - if not(media_stack): - if ( - not(target) - or ("armv7" in target and "android" in target) - or ("x86_64" in target) + if not media_stack: + if self.config["build"]["media-stack"] != "auto": + media_stack = self.config["build"]["media-stack"] + elif ( + not target + or ("armv7" in target and "android" in target) + or "x86_64" in target ): media_stack = "gstreamer" else: |