diff options
Diffstat (limited to 'python/servo/build_commands.py')
| -rw-r--r-- | python/servo/build_commands.py | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/python/servo/build_commands.py b/python/servo/build_commands.py index 4b0858f6ff1..d354ca02df4 100644 --- a/python/servo/build_commands.py +++ b/python/servo/build_commands.py @@ -62,8 +62,12 @@ class MachCommands(CommandBase): opts = params or [] has_media_stack = "media-gstreamer" in self.features - if build_type == BuildType.RELEASE: + if build_type.is_release(): opts += ["--release"] + elif build_type.is_dev(): + pass # there is no argument for debug + else: + opts += ["--profile", build_type.profile] if jobs is not None: opts += ["-j", jobs] |