author | wenzelm |
Thu, 10 Dec 2009 14:23:28 +0100 | |
changeset 34776 | 01a9bfd64b87 |
parent 34775 | 49245d68f7e4 |
child 34777 | 91d6089cef88 |
--- a/src/Tools/jEdit/src/proofdocument/html_panel.scala Thu Dec 10 14:14:49 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala Thu Dec 10 14:23:28 2009 +0100 @@ -51,7 +51,7 @@ private def try_file(name: String): String = { val file = sys.platform_file(name) - if (file.exists) Source.fromFile(file).mkString else "" + if (file.isFile) Source.fromFile(file).mkString else "" } private def template(font_size: Int): String =