Output 6.245 seconds instead of 6.0245 seconds

Author: AngledLuffa

src/edu/stanford/nlp/util/logging/Redwood.java

@@ -576,7 +576,7 @@ protected static void formatTimeDifference(long diff, StringBuilder b){
       b.append(min).append(':');
     }
     if (min > 0 && sec < 10) { b.append('0'); }
-    b.append(sec).append('.').append(String.format("%04d", mili));
+    b.append(sec).append('.').append(String.format("%03d", mili));
     if(min > 0) b.append(" minutes");
     else b.append(" seconds");
   }