equal
deleted
inserted
replaced
111 if (debug != null) { |
111 if (debug != null) { |
112 debug.println("Failed to use operating system seed " |
112 debug.println("Failed to use operating system seed " |
113 + "generator: " + e.toString()); |
113 + "generator: " + e.toString()); |
114 } |
114 } |
115 } |
115 } |
116 } else if (egdSource.length() != 0) { |
116 } else if (!egdSource.isEmpty()) { |
117 try { |
117 try { |
118 instance = new URLSeedGenerator(egdSource); |
118 instance = new URLSeedGenerator(egdSource); |
119 if (debug != null) { |
119 if (debug != null) { |
120 debug.println("Using URL seed generator reading from " |
120 debug.println("Using URL seed generator reading from " |
121 + egdSource); |
121 + egdSource); |