# 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" -