--- a/src/Tools/jEdit/etc/options Sat Jul 13 13:25:42 2013 +0200
+++ b/src/Tools/jEdit/etc/options Sat Jul 13 13:58:13 2013 +0200
@@ -76,18 +76,9 @@
section "Icons"
-(* jEdit/Tango *)
-(*
-option tooltip_close_icon : string = "16x16/actions/document-close.png"
-option tooltip_detach_icon : string = "16x16/actions/window-new.png"
-option gutter_warning_icon : string = "16x16/status/dialog-information.png"
-option gutter_legacy_icon : string = "16x16/status/dialog-warning.png"
-option gutter_error_icon : string = "16x16/status/dialog-error.png"
-*)
-
-(* IntelliJ IDEA *)
option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
+option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
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"