Add url_tail to final url.

mdenet · Oct 22, 2024 · 9c9a809 · 9c9a809
1 parent e4d23f9
commit 9c9a809
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/platform/src/ToolsManager.js b/platform/src/ToolsManager.js
@@ -35,13 +35,14 @@ class ToolManager {
                     toolUrl.url = url;
                 }
                 else{
+                    let url_tail = url.split('/')[1];
                     let url_port = this.getPort(url);
                     if (url_port != null){
                         let path = this.fetchPathByPort(url_port);
 
                         if(path != null){
                             let base_url = utility.getBaseURL();
-                            toolUrl.url = base_url + path;
+                            toolUrl.url = base_url + path + url_tail;
                         }
                     }
                     else{