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