# HG changeset patch
# User wenzelm
# Date 1426775080 -3600
# Node ID d743e0e53f41da1af3f07e43a65a7be42ee3d3bd
# Parent  e8ac10713682b261916c204341563a463e2ee5a1
tuned;

diff -r e8ac10713682 -r d743e0e53f41 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Thu Mar 19 12:36:55 2015 +0100
+++ b/src/HOL/Tools/etc/options	Thu Mar 19 15:24:40 2015 +0100
@@ -1,6 +1,6 @@
 (* :mode=isabelle-options: *)
 
-section {* Automatically tried tools *}
+section "Automatically tried tools"
 
 public option auto_time_start : real = 1.0
   -- "initial delay for automatically tried tools (seconds)"
diff -r e8ac10713682 -r d743e0e53f41 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Mar 19 12:36:55 2015 +0100
+++ b/src/Tools/jEdit/etc/options	Thu Mar 19 15:24:40 2015 +0100
@@ -141,4 +141,3 @@
 option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
 option process_passive_icon : string = "idea-icons/process/step_passive.png"
 option process_active_icons : string = "idea-icons/process/step_1.png:idea-icons/process/step_2.png:idea-icons/process/step_3.png:idea-icons/process/step_4.png:idea-icons/process/step_5.png:idea-icons/process/step_6.png:idea-icons/process/step_7.png:idea-icons/process/step_8.png:idea-icons/process/step_9.png:idea-icons/process/step_10.png:idea-icons/process/step_11.png:idea-icons/process/step_12.png"
-