src/Tools/jEdit/etc/options
changeset 52874 91032244e4ca
parent 52650 4cf6fbf1d9a1
child 53161 051cbf663b5f
--- a/src/Tools/jEdit/etc/options	Mon Aug 05 22:54:50 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Aug 05 23:57:29 2013 +0200
@@ -83,4 +83,6 @@
 option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
 option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
 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"