Configure devtools server via preferences

2025-08-07 14:35:33 +01:00 · 2020-07-17 08:31:26 +02:00 · 2020-07-17 08:31:26 +02:00 · 2c36754bf7
commit 2c36754bf7
parent b8d6b1d52d
5 changed files with 42 additions and 12 deletions
--- a/components/config/prefs.rs
+++ b/components/config/prefs.rs
@ -123,6 +123,12 @@ mod gen {
                    },
                },
            },
+            devtools: {
+                server: {
+                    enabled: bool,
+                    port: i64,
+                },
+            },
            dom: {
                webgpu: {
                    enabled: bool,