1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
Description: Providing DFSG-free icons to replace the non-free ones by Sun Mic.
Author: Pierre Gruet <pgt@debian.org>
Forwarded: not-needed
Last-Update: 2021-08-26
--- a/king/src/king/KingPrefs.java
+++ b/king/src/king/KingPrefs.java
@@ -108,19 +108,19 @@
// Icon that's displayed in the corner of the main window
windowIcon = new ImageIcon(getClass().getResource("images/kingicon20.png")).getImage();
- stepBackIcon = new ImageIcon(getClass().getResource("images/StepBack16.gif"));
- stepForwardIcon = new ImageIcon(getClass().getResource("images/StepForward16.gif"));
- moveUpIcon = new ImageIcon(getClass().getResource("images/Up16.gif"));
- moveDownIcon = new ImageIcon(getClass().getResource("images/Down16.gif"));
+ stepBackIcon = new ImageIcon(getClass().getResource("images/StepBack16.png"));
+ stepForwardIcon = new ImageIcon(getClass().getResource("images/StepForward16.png"));
+ moveUpIcon = new ImageIcon(getClass().getResource("images/Up16.png"));
+ moveDownIcon = new ImageIcon(getClass().getResource("images/Down16.png"));
basicDownIcon = new ImageIcon(getClass().getResource("images/DownBasic.gif"));
- addIcon = new ImageIcon(getClass().getResource("images/Add16.gif"));
- cutIcon = new ImageIcon(getClass().getResource("images/Cut16.gif"));
- copyIcon = new ImageIcon(getClass().getResource("images/Copy16.gif"));
- pasteIcon = new ImageIcon(getClass().getResource("images/Paste16.gif"));
- deleteIcon = new ImageIcon(getClass().getResource("images/Delete16.gif"));
- helpIcon = new ImageIcon(getClass().getResource("images/Help16.gif"));
- htmlBackIcon = new ImageIcon(getClass().getResource("images/Back24.gif"));
- htmlHomeIcon = new ImageIcon(getClass().getResource("images/Home24.gif"));
+ addIcon = new ImageIcon(getClass().getResource("images/Add16.png"));
+ cutIcon = new ImageIcon(getClass().getResource("images/Cut16.png"));
+ copyIcon = new ImageIcon(getClass().getResource("images/Copy16.png"));
+ pasteIcon = new ImageIcon(getClass().getResource("images/Paste16.png"));
+ deleteIcon = new ImageIcon(getClass().getResource("images/Delete16.png"));
+ helpIcon = new ImageIcon(getClass().getResource("images/Help16.png"));
+ htmlBackIcon = new ImageIcon(getClass().getResource("images/Back24.png"));
+ htmlHomeIcon = new ImageIcon(getClass().getResource("images/Home24.png"));
treeOnIcon = new ImageIcon(getClass().getResource("images/tree-on.png"));
treeOffIcon = new ImageIcon(getClass().getResource("images/tree-off.png"));
|
