src/Tools/jEdit/src/html_panel.scala
changeset 43669 9d34288e9351
parent 43661 39fdbd814c7f
child 45099 67740480cf39
     1.1 --- a/src/Tools/jEdit/src/html_panel.scala	Tue Jul 05 20:36:49 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Tue Jul 05 21:20:24 2011 +0200
     1.3 @@ -92,8 +92,7 @@
     1.4  <head>
     1.5  <style media="all" type="text/css">
     1.6  """ +
     1.7 -  Isabelle_System.try_read(
     1.8 -    Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
     1.9 +  Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
    1.10  
    1.11    private val template_tail =
    1.12  """