From 1a8c5fed6f53b2a4b5ed120193acd10a4ffcb2c6 Mon Sep 17 00:00:00 2001 From: Simon Sapin Date: Mon, 6 Jul 2020 17:34:17 +0200 Subject: [PATCH] Add `.servobuild` configuration for the choice of media stack --- python/servo/command_base.py | 13 ++++++++----- servobuild.example | 3 +++ 2 files changed, 11 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: diff --git a/servobuild.example b/servobuild.example index 59f61d10f66..7fdef6607b5 100644 --- a/servobuild.example +++ b/servobuild.example @@ -46,6 +46,9 @@ dom-backtrace = false # Default to the “2020” implementation of CSS layout instead of the “2013” one. layout-2020 = false +# Pick a media stack based on the target. Other values are "gstreamer" and "dummy" +media-stack = "auto" + # Set to the path to your ccache binary to enable caching of compiler outputs #ccache = "/usr/local/bin/ccache"