Configure devtools server via preferences

1 files changed, 9 insertions, 3 deletions

diff --git a/components/servo/lib.rs b/components/servo/lib.rs
index aa71c8f3309..581619e431a 100644
--- a/components/servo/lib.rs
+++ b/components/servo/lib.rs
@@ -393,9 +393,15 @@ where
         let mem_profiler_chan = profile_mem::Profiler::create(opts.mem_profiler_period);
 
         let debugger_chan = opts.debugger_port.map(|port| debugger::start_server(port));
-        let devtools_chan = opts
-            .devtools_port
-            .map(|port| devtools::start_server(port, embedder_proxy.clone()));
+
+        let devtools_chan = if opts.devtools_server_enabled {
+            Some(devtools::start_server(
+                opts.devtools_port,
+                embedder_proxy.clone(),
+            ))
+        } else {
+            None
+        };
 
         let coordinates = window.get_coordinates();
         let device_pixel_ratio = coordinates.hidpi_factor.get();