# HG changeset patch # User wenzelm # Date 1260308312 -3600 # Node ID 0c630c52fc7498822365b9392d1839086e4ae3a5 # Parent 826525fc5285bd0daaf5f06650826ea6878aff6b prefer options from running application; diff -r 826525fc5285 -r 0c630c52fc74 src/Tools/jEdit/src/proofdocument/html_panel.scala --- a/src/Tools/jEdit/src/proofdocument/html_panel.scala Tue Dec 08 21:54:34 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala Tue Dec 08 22:38:32 2009 +0100 @@ -43,10 +43,11 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -