Mirrors/servo
1
0
Fork 0
mirror of https://github.com/servo/servo.git synced 2025-06-28 19:13:41 +01:00
Code Issues Projects Releases Packages Wiki Activity

Add .servobuild configuration for the choice of media stack

Browse source
This commit is contained in:
Simon Sapin 2020-07-06 17:34:17 +02:00
parent 637c6c0aec
commit 1a8c5fed6f
2 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

13
python/servo/command_base.py
View file

@ -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: