From f006aa36d176d3f3a2cf21bf9e89c52bdd578e0e Mon Sep 17 00:00:00 2001
From: Calixte Denizet <calixte.denizet@gmail.com>
Date: Thu, 27 Jun 2024 18:57:00 +0200
Subject: [PATCH] Add a port option to gulp server

---
 gulpfile.mjs | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/gulpfile.mjs b/gulpfile.mjs
index ee966b2ed45b7..58fc024049397 100644
--- a/gulpfile.mjs
+++ b/gulpfile.mjs
@@ -2076,8 +2076,19 @@ gulp.task(
       console.log();
       console.log("### Starting local server");
 
+      let port = 8888;
+      const i = process.argv.indexOf("--port");
+      if (i >= 0 && i + 1 < process.argv.length) {
+        const p = parseInt(process.argv[i + 1], 10);
+        if (!isNaN(p)) {
+          port = p;
+        } else {
+          console.error("Invalid port number: using default (8888)");
+        }
+      }
+
       const { WebServer } = await import("./test/webserver.mjs");
-      const server = new WebServer({ port: 8888 });
+      const server = new WebServer({ port });
       server.start();
     }
   )