# HG changeset patch # User wenzelm # Date 1383993692 -3600 # Node ID 4fac53028f874b026504152bbbfa60cee63c2e2f # Parent 72254819befd4260c8c429bd20b996479d46239f adjust modules for Admin/build jars_test; diff -r 72254819befd -r 4fac53028f87 src/Pure/GUI/system_dialog.scala --- a/src/Pure/GUI/system_dialog.scala Sat Nov 09 11:24:21 2013 +0100 +++ b/src/Pure/GUI/system_dialog.scala Sat Nov 09 11:41:32 2013 +0100 @@ -1,5 +1,4 @@ /* Title: Pure/GUI/system_dialog.scala - Module: PIDE-GUI Author: Makarius Dialog for system processes, with optional output window. diff -r 72254819befd -r 4fac53028f87 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Sat Nov 09 11:24:21 2013 +0100 +++ b/src/Pure/Thy/html.scala Sat Nov 09 11:41:32 2013 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/Thy/html.scala + Module: PIDE-GUI Author: Makarius HTML presentation elements.