src/Tools/jEdit/src/plugin.scala
changeset 66351 95847ffa62dc
parent 66083 dcc685d5c3f7
child 66458 42d0d5c77c78
--- a/src/Tools/jEdit/src/plugin.scala	Sun Aug 06 17:32:32 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Aug 06 17:38:54 2017 +0200
@@ -12,7 +12,6 @@
 import javax.swing.JOptionPane
 
 import java.io.{File => JFile}
-import java.util.UUID
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
 import org.gjt.sp.jedit.textarea.JEditTextArea
@@ -398,7 +397,7 @@
 
   /* HTTP server */
 
-  val http_root: String = "/" + UUID.randomUUID().toString
+  val http_root: String = "/" + Library.UUID()
 
   val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))