mirror of
https://github.com/servo/servo.git
synced 2025-06-21 23:59:00 +01:00
Fixed #6048
This commit is contained in:
parent
8faa9f877d
commit
8af4e10086
1 changed files with 11 additions and 0 deletions
|
@ -137,11 +137,22 @@ class MachCommands(CommandBase):
|
||||||
opts = params or []
|
opts = params or []
|
||||||
features = []
|
features = []
|
||||||
|
|
||||||
|
base_path = path.join("components", "servo", "target")
|
||||||
|
release_path = path.join(base_path, "release", "servo")
|
||||||
|
dev_path = path.join(base_path, "debug", "servo")
|
||||||
|
|
||||||
|
release_exists = path.exists(release_path)
|
||||||
|
dev_exists = path.exists(dev_path)
|
||||||
|
|
||||||
if not (release or dev):
|
if not (release or dev):
|
||||||
if self.config["build"]["mode"] == "dev":
|
if self.config["build"]["mode"] == "dev":
|
||||||
dev = True
|
dev = True
|
||||||
elif self.config["build"]["mode"] == "release":
|
elif self.config["build"]["mode"] == "release":
|
||||||
release = True
|
release = True
|
||||||
|
elif release_exists and not dev_exists:
|
||||||
|
release = True
|
||||||
|
elif dev_exists and not release_exists:
|
||||||
|
dev = True
|
||||||
else:
|
else:
|
||||||
print("Please specify either --dev (-d) for a development")
|
print("Please specify either --dev (-d) for a development")
|
||||||
print(" build, or --release (-r) for an optimized build.")
|
print(" build, or --release (-r) for an optimized build.")
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue