X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flib%2Flib.c;h=17b0a8086e174a65595bcc11c879fe531a69ae15;hb=04a688940693c2286530386c05f2c8465da1a6a9;hp=42ca2fd69bdd25c66b33d1d5601fcea1a6b46cf8;hpb=df515c68cfb3a5785a3c1eac7857452769cd48f5;p=pintos-anon

diff --git a/src/lib/lib.c b/src/lib/lib.c
index 42ca2fd..17b0a80 100644
--- a/src/lib/lib.c
+++ b/src/lib/lib.c
@@ -369,7 +369,7 @@ printf_integer (uintmax_t value, bool negative, const char *digits,
   char buf[64], *cp;
   int base;
   const char *base_name;
-  int pad_cnt;
+  int pad_cnt, group_cnt;
 
   base = strlen (digits);
 
@@ -378,10 +378,14 @@ printf_integer (uintmax_t value, bool negative, const char *digits,
      will output the buffer's content in reverse.  This is also
      the reason that later we append zeros and the sign. */
   cp = buf;
+  group_cnt = 0;
   while (value > 0) 
     {
-      if ((c->flags & GROUP) && cp > buf && (cp - buf) % 3 == 0)
-        *cp++ = ',';
+      if ((c->flags & GROUP) && group_cnt++ == 3) 
+        {
+          *cp++ = ',';
+          group_cnt = 0; 
+        }
       *cp++ = digits[value % base];
       value /= base;
     }