src/Tools/jEdit/src/html_panel.scala
changeset 43606 e1a09c2a6248
parent 43551 07a9cbf2376f
child 43661 39fdbd814c7f
     1.1 --- a/src/Tools/jEdit/src/html_panel.scala	Thu Jun 30 14:51:32 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Thu Jun 30 14:55:01 2011 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4  <head>
     1.5  <style media="all" type="text/css">
     1.6  """ +
     1.7 -  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
     1.8 +  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
     1.9  
    1.10    private val template_tail =
    1.11  """